attribute code_abbrev superseedes code_unfold_post; tuned names and spacing
authorhaftmann
Thu Dec 29 10:47:55 2011 +0100 (2011-12-29)
changeset 460294a19e3d147c3
parent 46028 9f113cdf3d66
child 46030 51b2f3412a03
attribute code_abbrev superseedes code_unfold_post; tuned names and spacing
src/HOL/Imperative_HOL/Heap_Monad.thy
     1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Dec 29 10:47:55 2011 +0100
     1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Dec 29 10:47:55 2011 +0100
     1.3 @@ -168,19 +168,19 @@
     1.4    shows "a = b" and "h' = h''"
     1.5    using assms unfolding effect_def by auto
     1.6  
     1.7 -ML {* structure Crel_Intros = Named_Thms
     1.8 +ML {* structure Effect_Intros = Named_Thms
     1.9  (
    1.10    val name = @{binding effect_intros}
    1.11    val description = "introduction rules for effect"
    1.12  ) *}
    1.13  
    1.14 -ML {* structure Crel_Elims = Named_Thms
    1.15 +ML {* structure Effect_Elims = Named_Thms
    1.16  (
    1.17    val name = @{binding effect_elims}
    1.18    val description = "elimination rules for effect"
    1.19  ) *}
    1.20  
    1.21 -setup "Crel_Intros.setup #> Crel_Elims.setup"
    1.22 +setup "Effect_Intros.setup #> Effect_Elims.setup"
    1.23  
    1.24  lemma effect_LetI [effect_intros]:
    1.25    assumes "x = t" "effect (f x) h h' r"
    1.26 @@ -447,7 +447,7 @@
    1.27    using assms unfolding Heap_ord_def img_ord_def fun_ord_def flat_ord_def
    1.28    by atomize_elim blast
    1.29  
    1.30 -lemma bind_mono[partial_function_mono]:
    1.31 +lemma bind_mono [partial_function_mono]:
    1.32    assumes mf: "mono_Heap B" and mg: "\<And>y. mono_Heap (\<lambda>f. C y f)"
    1.33    shows "mono_Heap (\<lambda>f. B f \<guillemotright>= (\<lambda>y. C y f))"
    1.34  proof (rule monotoneI)
    1.35 @@ -496,10 +496,10 @@
    1.36  definition raise' :: "String.literal \<Rightarrow> 'a Heap" where
    1.37    [code del]: "raise' s = raise (explode s)"
    1.38  
    1.39 -lemma [code_post]: "raise' (STR s) = raise s"
    1.40 -unfolding raise'_def by (simp add: STR_inverse)
    1.41 +lemma [code_abbrev]: "raise' (STR s) = raise s"
    1.42 +  unfolding raise'_def by (simp add: STR_inverse)
    1.43  
    1.44 -lemma raise_raise' [code_unfold]:
    1.45 +lemma raise_raise': (* FIXME delete candidate *)
    1.46    "raise s = raise' (STR s)"
    1.47    unfolding raise'_def by (simp add: STR_inverse)
    1.48