Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Imperative_HOL/Heap_Monad.thy
changeset 59028 df7476e79558
parent 58939 994fe0ba8335
child 59058 a78612c67ec0 
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Nov 21 22:59:32 2014 +0100
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Sat Nov 22 11:36:00 2014 +0100
@@ -154,7 +154,7 @@
   using assms unfolding effect_def by auto
 
 named_theorems effect_intros "introduction rules for effect"
-named_theorems effect_elims "elimination rules for effect"
+  and effect_elims "elimination rules for effect"
 
 lemma effect_LetI [effect_intros]:
   assumes "x = t" "effect (f x) h h' r"
isabelle