# 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 \ c \ c' = (\i s stk. c = (i,s,stk) \ c' = iexec(P!!i) (i,s,stk) \ 0 \ i \ i < size P)" -(* -declare exec1_def [simp] -*) - lemma exec1I [intro, code_pred_intro]: "c' = iexec (P!!i) (i,s,stk) \ 0 \ i \ i < size P \ P \ (i,s,stk) \ c'"