avoid ambiguities; tuned
authorhaftmann
Wed Jul 14 16:45:30 2010 +0200 (2010-07-14)
changeset 378289e1758c7ff06
parent 37827 954c9ce1d333
child 37829 11f813e86305
avoid ambiguities; tuned
src/HOL/Imperative_HOL/Heap_Monad.thy
src/HOL/Imperative_HOL/ex/Linked_Lists.thy
     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  
     2.1 --- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Wed Jul 14 16:45:29 2010 +0200
     2.2 +++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Wed Jul 14 16:45:30 2010 +0200
     2.3 @@ -550,7 +550,7 @@
     2.4    }"
     2.5    unfolding rev'_def MREC_rule[of _ _ "(q, p)"] unfolding rev'_def[symmetric]
     2.6  thm arg_cong2
     2.7 -  by (auto simp add: expand_fun_eq intro: arg_cong2[where f = "op \<guillemotright>="] split: node.split)
     2.8 +  by (auto simp add: expand_fun_eq intro: arg_cong2[where f = bind] split: node.split)
     2.9  
    2.10  primrec rev :: "('a:: heap) node \<Rightarrow> 'a node Heap" 
    2.11  where