# HG changeset patch
# User kleing
# Date 1376044049 -7200
# Node ID 9587134ec780e453856ab12c43b683467de4291c
# Parent  ec63c82551aefce14de0b957ed49b1a393b90c5d
removed commented out declaration

diff -r ec63c82551ae -r 9587134ec780 src/HOL/IMP/Compiler.thy
--- a/src/HOL/IMP/Compiler.thy	Fri Aug 09 11:26:29 2013 +0200
+++ b/src/HOL/IMP/Compiler.thy	Fri Aug 09 12:27:29 2013 +0200
@@ -63,10 +63,6 @@
   "P \<turnstile> c \<rightarrow> c' = 
   (\<exists>i s stk. c = (i,s,stk) \<and> c' = iexec(P!!i) (i,s,stk) \<and> 0 \<le> i \<and> i < size P)"
 
-(*
-declare exec1_def [simp]
-*)
-
 lemma exec1I [intro, code_pred_intro]:
   "c' = iexec (P!!i) (i,s,stk) \<Longrightarrow> 0 \<le> i \<Longrightarrow> i < size P
   \<Longrightarrow> P \<turnstile> (i,s,stk) \<rightarrow> c'"