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/Mrec.thy
changeset 37787 30dc3abf4a58
parent 37772 026ed2fc15d4
child 37792 ba0bc31b90d7 
--- a/src/HOL/Imperative_HOL/Mrec.thy	Tue Jul 13 02:29:05 2010 +0200
+++ b/src/HOL/Imperative_HOL/Mrec.thy	Tue Jul 13 11:38:03 2010 +0200
@@ -76,7 +76,7 @@
   apply simp
   apply (rule ext)
   apply (unfold mrec_rule[of x])
-  by (auto split: option.splits prod.splits sum.splits)
+  by (auto simp add: execute_simps split: option.splits prod.splits sum.splits)
 
 lemma MREC_pinduct:
   assumes "execute (MREC x) h = Some (r, h')"
isabelle