summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Sat, 16 Aug 2014 18:08:55 +0200 | |

changeset 57956 | 3ab5d15fac6b |

parent 57955 | f28337c2c0a8 |

child 57957 | e6ee35b8f4b5 |

updated to named_theorems;

--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Sat Aug 16 16:45:39 2014 +0200 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Sat Aug 16 18:08:55 2014 +0200 @@ -39,13 +39,7 @@ "(\<And>h. execute f h = execute g h) \<Longrightarrow> f = g" by (cases f, cases g) (auto simp: fun_eq_iff) -ML {* structure Execute_Simps = Named_Thms -( - val name = @{binding execute_simps} - val description = "simplification rules for execute" -) *} - -setup Execute_Simps.setup +named_theorems execute_simps "simplification rules for execute" lemma execute_Let [execute_simps]: "execute (let x = t in f x) = (let x = t in execute (f x))" @@ -93,13 +87,7 @@ and "execute f h \<noteq> None" using assms by (simp add: success_def) -ML {* structure Success_Intros = Named_Thms -( - val name = @{binding success_intros} - val description = "introduction rules for success" -) *} - -setup Success_Intros.setup +named_theorems success_intros "introduction rules for success" lemma success_tapI [success_intros]: "success (tap f) h" @@ -167,19 +155,8 @@ shows "a = b" and "h' = h''" using assms unfolding effect_def by auto -ML {* structure Effect_Intros = Named_Thms -( - val name = @{binding effect_intros} - val description = "introduction rules for effect" -) *} - -ML {* structure Effect_Elims = Named_Thms -( - val name = @{binding effect_elims} - val description = "elimination rules for effect" -) *} - -setup "Effect_Intros.setup #> Effect_Elims.setup" +named_theorems effect_intros "introduction rules for effect" +named_theorems effect_elims "elimination rules for effect" lemma effect_LetI [effect_intros]: assumes "x = t" "effect (f x) h h' r"