src/HOL/Imperative_HOL/Heap_Monad.thy
changeset 37828 9e1758c7ff06
parent 37816 e550439d4422
child 37831 fa3a2e35c4f1
     1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Wed Jul 14 16:45:29 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Wed Jul 14 16:45:30 2010 +0200
     1.3 @@ -311,7 +311,7 @@
     1.4  lemma bind_return [simp]: "f \<guillemotright>= return = f"
     1.5    by (rule Heap_eqI) (simp add: bind_def execute_simps split: option.splits)
     1.6  
     1.7 -lemma bind_bind [simp]: "(f \<guillemotright>= g) \<guillemotright>= k = f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= k)"
     1.8 +lemma bind_bind [simp]: "(f \<guillemotright>= g) \<guillemotright>= k = (f :: 'a Heap) \<guillemotright>= (\<lambda>x. g x \<guillemotright>= k)"
     1.9    by (rule Heap_eqI) (simp add: bind_def execute_simps split: option.splits)
    1.10  
    1.11  lemma raise_bind [simp]: "raise e \<guillemotright>= f = raise e"
    1.12 @@ -410,14 +410,14 @@
    1.13  subsubsection {* SML and OCaml *}
    1.14  
    1.15  code_type Heap (SML "unit/ ->/ _")
    1.16 -code_const "op \<guillemotright>=" (SML "!(fn/ f'_/ =>/ fn/ ()/ =>/ f'_/ (_/ ())/ ())")
    1.17 +code_const bind (SML "!(fn/ f'_/ =>/ fn/ ()/ =>/ f'_/ (_/ ())/ ())")
    1.18  code_const return (SML "!(fn/ ()/ =>/ _)")
    1.19  code_const Heap_Monad.raise' (SML "!(raise/ Fail/ _)")
    1.20  
    1.21  code_type Heap (OCaml "unit/ ->/ _")
    1.22 -code_const "op \<guillemotright>=" (OCaml "!(fun/ f'_/ ()/ ->/ f'_/ (_/ ())/ ())")
    1.23 +code_const bind (OCaml "!(fun/ f'_/ ()/ ->/ f'_/ (_/ ())/ ())")
    1.24  code_const return (OCaml "!(fun/ ()/ ->/ _)")
    1.25 -code_const Heap_Monad.raise' (OCaml "failwith/ _")
    1.26 +code_const Heap_Monad.raise' (OCaml "failwith")
    1.27  
    1.28  setup {*
    1.29  
    1.30 @@ -530,7 +530,7 @@
    1.31  code_type Heap (Haskell "Heap.ST/ Heap.RealWorld/ _")
    1.32  code_monad bind Haskell
    1.33  code_const return (Haskell "return")
    1.34 -code_const Heap_Monad.raise' (Haskell "error/ _")
    1.35 +code_const Heap_Monad.raise' (Haskell "error")
    1.36  
    1.37  hide_const (open) Heap heap guard raise' fold_map
    1.38