| changeset 55836 | 8093590e49e4 |
| parent 55834 | 459b5561ba4e |
| child 58889 | 5b7a9633cfa8 |
--- a/src/HOL/IMP/Small_Step.thy Sun Mar 02 18:41:41 2014 +0100 +++ b/src/HOL/IMP/Small_Step.thy Sun Mar 02 19:15:23 2014 +0100 @@ -159,7 +159,7 @@ lemma small_to_big: "cs \<rightarrow>* (SKIP,t) \<Longrightarrow> cs \<Rightarrow> t" -apply (induction cs "(SKIP,t)" arbitrary: t rule: star.induct) +apply (induction cs "(SKIP,t)" rule: star.induct) apply (auto intro: small1_big_continue) done