diff options
| author | Christopher Pulte | 2016-12-09 15:02:47 +0000 |
|---|---|---|
| committer | Christopher Pulte | 2016-12-09 15:02:47 +0000 |
| commit | 66f2498b28fe4a9be40c2b4093f64827a146f371 (patch) | |
| tree | 40cac4e1c024638f5ade988ba235b41c7d619b7a /mips/mips_extras_embed.lem | |
| parent | 1495ba7749f9678c36e5fe130948d425d2a345ff (diff) | |
sail changes for making lem embedding Isabelle-friendlier
Diffstat (limited to 'mips/mips_extras_embed.lem')
| -rw-r--r-- | mips/mips_extras_embed.lem | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mips/mips_extras_embed.lem b/mips/mips_extras_embed.lem index d59213b8..41a6726f 100644 --- a/mips/mips_extras_embed.lem +++ b/mips/mips_extras_embed.lem @@ -33,9 +33,9 @@ val MEMval_tag : (vector bitU * integer * vector bitU) -> M unit val MEMval_tag_conditional : (vector bitU * integer * vector bitU) -> M bitU let MEMval (_,_,v) = write_mem_val endian v >>= fun _ -> return () -let MEMval_conditional (_,_,v) = write_mem_val endian v >>= fun b -> return (if b then I else O) +let MEMval_conditional (_,_,v) = write_mem_val endian v >>= fun b -> return (if b then B1 else B0) let MEMval_tag (_,_,v) = write_mem_val endian v >>= fun _ -> return () -let MEMval_tag_conditional (_,_,v) = write_mem_val endian v >>= fun b -> return (if b then I else O) +let MEMval_tag_conditional (_,_,v) = write_mem_val endian v >>= fun b -> return (if b then B1 else B0) val MEM_sync : unit -> M unit |