# HG changeset patch
# User nipkow
# Date 1441875809 -7200
# Node ID 263a354329e913c0edf792d842e342563d77b4bd
# Parent  6fced6d926be1c45b20cc05f59500d0fad5cda87
tuned

diff -r 6fced6d926be -r 263a354329e9 src/HOL/IMP/Compiler.thy
--- a/src/HOL/IMP/Compiler.thy	Wed Sep 09 23:01:27 2015 +0200
+++ b/src/HOL/IMP/Compiler.thy	Thu Sep 10 11:03:29 2015 +0200
@@ -81,8 +81,6 @@
 where
   "exec P \<equiv> star (exec1 P)"
 
-declare star.step[intro]
-
 lemmas exec_induct = star.induct [of "exec1 P", split_format(complete)]
 
 code_pred exec1 by (metis exec1_def)
@@ -107,7 +105,7 @@
 by (auto simp: exec1_def)
 
 lemma exec_appendR: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow>* c'"
-by (induction rule: star.induct) (fastforce intro: exec1_appendR)+
+by (induction rule: star.induct) (fastforce intro: star.step exec1_appendR)+
 
 lemma exec1_appendL:
   fixes i i' :: int 
@@ -122,7 +120,7 @@
   shows
  "P \<turnstile> (i,s,stk) \<rightarrow>* (i',s',stk')  \<Longrightarrow>
   P' @ P \<turnstile> (size(P')+i,s,stk) \<rightarrow>* (size(P')+i',s',stk')"
-  by (induction rule: exec_induct) (blast intro!: exec1_appendL)+
+  by (induction rule: exec_induct) (blast intro: star.step exec1_appendL)+
 
 text{* Now we specialise the above lemmas to enable automatic proofs of
 @{prop "P \<turnstile> c \<rightarrow>* c'"} where @{text P} is a mixture of concrete instructions and
diff -r 6fced6d926be -r 263a354329e9 src/HOL/IMP/Compiler2.thy
--- a/src/HOL/IMP/Compiler2.thy	Wed Sep 09 23:01:27 2015 +0200
+++ b/src/HOL/IMP/Compiler2.thy	Thu Sep 10 11:03:29 2015 +0200
@@ -44,7 +44,7 @@
 
 lemma exec_n_exec:
   "P \<turnstile> c \<rightarrow>^n c' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c'"
-  by (induct n arbitrary: c) auto
+  by (induct n arbitrary: c) (auto intro: star.step)
 
 lemma exec_0 [intro!]: "P \<turnstile> c \<rightarrow>^0 c" by simp