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')"