changeset 37878 d016aaead7a2 parent 37845 b70d7a347964 child 37947 844977c7abeb
```     1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Jul 19 11:55:42 2010 +0200
1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Jul 19 11:55:42 2010 +0200
1.3 @@ -124,10 +124,10 @@
1.4  *}
1.5
1.6  definition crel :: "'a Heap \<Rightarrow> heap \<Rightarrow> heap \<Rightarrow> 'a \<Rightarrow> bool" where
1.7 -  crel_def: "crel c h h' r \<longleftrightarrow> Heap_Monad.execute c h = Some (r, h')"
1.8 +  crel_def: "crel c h h' r \<longleftrightarrow> execute c h = Some (r, h')"
1.9
1.10  lemma crelI:
1.11 -  "Heap_Monad.execute c h = Some (r, h') \<Longrightarrow> crel c h h' r"
1.12 +  "execute c h = Some (r, h') \<Longrightarrow> crel c h h' r"
1.14
1.15  lemma crelE:
1.16 @@ -300,9 +300,9 @@
1.17    using assms by (auto simp add: crel_def bind_def split: option.split_asm)
1.18
1.19  lemma execute_bind_eq_SomeI:
1.20 -  assumes "Heap_Monad.execute f h = Some (x, h')"
1.21 -    and "Heap_Monad.execute (g x) h' = Some (y, h'')"
1.22 -  shows "Heap_Monad.execute (f \<guillemotright>= g) h = Some (y, h'')"
1.23 +  assumes "execute f h = Some (x, h')"
1.24 +    and "execute (g x) h' = Some (y, h'')"
1.25 +  shows "execute (f \<guillemotright>= g) h = Some (y, h'')"
1.26    using assms by (simp add: bind_def)
1.27
1.28  lemma return_bind [simp]: "return x \<guillemotright>= f = f x"
1.29 @@ -487,7 +487,7 @@
1.30  code_reserved Scala Heap
1.31
1.32  code_type Heap (Scala "Unit/ =>/ _")
1.33 -code_const bind (Scala "!Heap.bind((_), (_))")
1.34 +code_const bind (Scala "bind")
1.35  code_const return (Scala "('_: Unit)/ =>/ _")