updated to named_theorems;
authorwenzelm
Sat Aug 16 18:08:55 2014 +0200 (2014-08-16)
changeset 579563ab5d15fac6b
parent 57955 f28337c2c0a8
child 57957 e6ee35b8f4b5
updated to named_theorems;
src/HOL/Imperative_HOL/Heap_Monad.thy
     1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Sat Aug 16 16:45:39 2014 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Sat Aug 16 18:08:55 2014 +0200
     1.3 @@ -39,13 +39,7 @@
     1.4    "(\<And>h. execute f h = execute g h) \<Longrightarrow> f = g"
     1.5      by (cases f, cases g) (auto simp: fun_eq_iff)
     1.6  
     1.7 -ML {* structure Execute_Simps = Named_Thms
     1.8 -(
     1.9 -  val name = @{binding execute_simps}
    1.10 -  val description = "simplification rules for execute"
    1.11 -) *}
    1.12 -
    1.13 -setup Execute_Simps.setup
    1.14 +named_theorems execute_simps "simplification rules for execute"
    1.15  
    1.16  lemma execute_Let [execute_simps]:
    1.17    "execute (let x = t in f x) = (let x = t in execute (f x))"
    1.18 @@ -93,13 +87,7 @@
    1.19      and "execute f h \<noteq> None"
    1.20    using assms by (simp add: success_def)
    1.21  
    1.22 -ML {* structure Success_Intros = Named_Thms
    1.23 -(
    1.24 -  val name = @{binding success_intros}
    1.25 -  val description = "introduction rules for success"
    1.26 -) *}
    1.27 -
    1.28 -setup Success_Intros.setup
    1.29 +named_theorems success_intros "introduction rules for success"
    1.30  
    1.31  lemma success_tapI [success_intros]:
    1.32    "success (tap f) h"
    1.33 @@ -167,19 +155,8 @@
    1.34    shows "a = b" and "h' = h''"
    1.35    using assms unfolding effect_def by auto
    1.36  
    1.37 -ML {* structure Effect_Intros = Named_Thms
    1.38 -(
    1.39 -  val name = @{binding effect_intros}
    1.40 -  val description = "introduction rules for effect"
    1.41 -) *}
    1.42 -
    1.43 -ML {* structure Effect_Elims = Named_Thms
    1.44 -(
    1.45 -  val name = @{binding effect_elims}
    1.46 -  val description = "elimination rules for effect"
    1.47 -) *}
    1.48 -
    1.49 -setup "Effect_Intros.setup #> Effect_Elims.setup"
    1.50 +named_theorems effect_intros "introduction rules for effect"
    1.51 +named_theorems effect_elims "elimination rules for effect"
    1.52  
    1.53  lemma effect_LetI [effect_intros]:
    1.54    assumes "x = t" "effect (f x) h h' r"