# HG changeset patch
# User bulwahn
# Date 1349858913 -7200
# Node ID 2a1dcc962005687a17132f154f54b4cf62cfba17
# Parent  65318db3087b667319460508e1493d8f51c51b9f
special code setup for step function in IMP is redundant as definition was tuned (cf. c54d901d2946)

diff -r 65318db3087b -r 2a1dcc962005 src/HOL/IMP/Collecting_Examples.thy
--- a/src/HOL/IMP/Collecting_Examples.thy	Wed Oct 10 10:48:17 2012 +0200
+++ b/src/HOL/IMP/Collecting_Examples.thy	Wed Oct 10 10:48:33 2012 +0200
@@ -7,12 +7,6 @@
 lemma insert_code [code]:  "insert x (set xs) = set (x#xs)"
 by simp
 
-text{* Make assignment rule executable: *}
-declare step.simps(2)[code del]
-lemma [code]: "step S (x ::= e {P}) = (x ::= e {(%s. s(x := aval e s)) ` S})"
-by auto
-declare step.simps(1,3-)[code]
-
 text{* The example: *}
 definition "c = WHILE Less (V ''x'') (N 3)
                 DO ''x'' ::= Plus (V ''x'') (N 2)"