# HG changeset patch # User nipkow # Date 1393784123 -3600 # Node ID 8093590e49e45d98fdce19b7cd122cf6656dd8db # Parent eb8e231a335fe136c88f14717609911cfd143b1e tuned proof diff -r eb8e231a335f -r 8093590e49e4 src/HOL/IMP/Small_Step.thy --- 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 \* (SKIP,t) \ cs \ 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