# HG changeset patch
# User nipkow
# Date 1393782086 -3600
# Node ID 459b5561ba4e7670adacf0b63f258565c5d59aae
# Parent  3a9386b32211c9b2027add8dc7b3ded65bf3126c
tuned proofs

diff -r 3a9386b32211 -r 459b5561ba4e src/HOL/IMP/Small_Step.thy
--- a/src/HOL/IMP/Small_Step.thy	Sun Mar 02 00:05:35 2014 +0100
+++ b/src/HOL/IMP/Small_Step.thy	Sun Mar 02 18:41:26 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:
 *}