# HG changeset patch
# User kleing
# Date 1378017484 -36000
# Node ID c5a1629d8e4504c43ef9df484094c6b74f5117d6
# Parent  603e6e97c391217ab8241fa998e076f3c47ba12d
remove redundant (simp del: ..)

diff -r 603e6e97c391 -r c5a1629d8e45 src/HOL/IMP/Compiler2.thy
--- a/src/HOL/IMP/Compiler2.thy	Sun Sep 01 00:37:53 2013 +0200
+++ b/src/HOL/IMP/Compiler2.thy	Sun Sep 01 16:38:04 2013 +1000
@@ -40,7 +40,7 @@
 
 lemma exec_n_exec:
   "P \<turnstile> c \<rightarrow>^n c' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c'"
-  by (induct n arbitrary: c) (auto simp del: exec1_def)
+  by (induct n arbitrary: c) auto
 
 lemma exec_0 [intro!]: "P \<turnstile> c \<rightarrow>^0 c" by simp
 
@@ -360,7 +360,7 @@
   obtain i' s'' stk'' where
     step: "P @ P' \<turnstile> (i, s, stk) \<rightarrow> (i', s'', stk'')" and
     rest: "P @ P' \<turnstile> (i', s'', stk'') \<rightarrow>^k (n, s', stk')"
-    by (auto simp del: exec1_def)
+    by auto
   from step `size P \<le> i`
   have "P' \<turnstile> (i - size P, s, stk) \<rightarrow> (i' - size P, s'', stk'')" 
     by (rule exec1_drop_left)