dropped superfluous prefixes
authorhaftmann
Mon Jul 19 11:55:42 2010 +0200 (2010-07-19)
changeset 37878d016aaead7a2
parent 37877 d4a30d210220
child 37879 443909380077
dropped superfluous prefixes
src/HOL/Imperative_HOL/Heap_Monad.thy
src/HOL/Imperative_HOL/Ref.thy
src/HOL/Library/Efficient_Nat.thy
     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.13    by (simp add: crel_def)
    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)/ =>/ _")
    1.36  code_const Heap_Monad.raise' (Scala "!error((_))")
    1.37  
     2.1 --- a/src/HOL/Imperative_HOL/Ref.thy	Mon Jul 19 11:55:42 2010 +0200
     2.2 +++ b/src/HOL/Imperative_HOL/Ref.thy	Mon Jul 19 11:55:42 2010 +0200
     2.3 @@ -296,11 +296,11 @@
     2.4  
     2.5  text {* Scala *}
     2.6  
     2.7 -code_type ref (Scala "!Heap.Ref[_]")
     2.8 +code_type ref (Scala "!Ref[_]")
     2.9  code_const Ref (Scala "!error(\"bare Ref\")")
    2.10 -code_const ref (Scala "('_: Unit)/ =>/ Heap.Ref((_))")
    2.11 -code_const Ref.lookup (Scala "('_: Unit)/ =>/ Heap.lookup((_))")
    2.12 -code_const Ref.update (Scala "('_: Unit)/ =>/ Heap.update((_), (_))")
    2.13 +code_const ref (Scala "('_: Unit)/ =>/ Ref((_))")
    2.14 +code_const Ref.lookup (Scala "('_: Unit)/ =>/ lookup((_))")
    2.15 +code_const Ref.update (Scala "('_: Unit)/ =>/ update((_), (_))")
    2.16  
    2.17  end
    2.18  
     3.1 --- a/src/HOL/Library/Efficient_Nat.thy	Mon Jul 19 11:55:42 2010 +0200
     3.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Mon Jul 19 11:55:42 2010 +0200
     3.3 @@ -337,7 +337,7 @@
     3.4  
     3.5  code_type nat
     3.6    (Haskell "Nat.Nat")
     3.7 -  (Scala "Nat.Nat")
     3.8 +  (Scala "Nat")
     3.9  
    3.10  code_instance nat :: eq
    3.11    (Haskell -)
    3.12 @@ -405,7 +405,7 @@
    3.13  
    3.14  code_const int and nat
    3.15    (Haskell "toInteger" and "fromInteger")
    3.16 -  (Scala "!_.as'_BigInt" and "!Nat.Nat((_))")
    3.17 +  (Scala "!_.as'_BigInt" and "Nat")
    3.18  
    3.19  text {* Conversion from and to indices. *}
    3.20  
    3.21 @@ -419,7 +419,7 @@
    3.22    (SML "IntInf.fromInt")
    3.23    (OCaml "_")
    3.24    (Haskell "toEnum")
    3.25 -  (Scala "!Nat.Nat((_))")
    3.26 +  (Scala "Nat")
    3.27  
    3.28  text {* Using target language arithmetic operations whenever appropriate *}
    3.29