# HG changeset patch
# User nipkow
# Date 1393782101 -3600
# Node ID eb8e231a335fe136c88f14717609911cfd143b1e
# Parent  6fe16c8a647483b8c5b2226c1cb827d374fdb674# Parent  459b5561ba4e7670adacf0b63f258565c5d59aae
merged

diff -r 6fe16c8a6474 -r eb8e231a335f src/HOL/IMP/Small_Step.thy
--- a/src/HOL/IMP/Small_Step.thy	Sun Mar 02 18:20:08 2014 +0100
+++ b/src/HOL/IMP/Small_Step.thy	Sun Mar 02 18:41:41 2014 +0100
@@ -157,15 +157,12 @@
 apply auto
 done
 
-lemma small_big_continue:
-  "cs \<rightarrow>* cs' \<Longrightarrow> cs' \<Rightarrow> t \<Longrightarrow> cs \<Rightarrow> t"
-apply (induction rule: star.induct)
+lemma small_to_big:
+  "cs \<rightarrow>* (SKIP,t) \<Longrightarrow> cs \<Rightarrow> t"
+apply (induction cs "(SKIP,t)" arbitrary: t rule: star.induct)
 apply (auto intro: small1_big_continue)
 done
 
-lemma small_to_big: "cs \<rightarrow>* (SKIP,t) \<Longrightarrow> cs \<Rightarrow> t"
-by (metis small_big_continue Skip)
-
 text {*
   Finally, the equivalence theorem:
 *}