1.1 --- a/src/HOL/IMP/Compiler.thy	Wed Oct 23 16:10:42 2002 +0200
     1.2 +++ b/src/HOL/IMP/Compiler.thy	Thu Oct 24 07:23:46 2002 +0200
     1.3 @@ -11,11 +11,11 @@
     1.4  consts compile :: "com \<Rightarrow> instr list"
     1.5  primrec
     1.6  "compile \<SKIP> = []"
     1.7 -"compile (x:==a) = [ASIN x a]"
     1.8 +"compile (x:==a) = [SET x a]"
     1.9  "compile (c1;c2) = compile c1 @ compile c2"
    1.10  "compile (\<IF> b \<THEN> c1 \<ELSE> c2) =
    1.11   [JMPF b (length(compile c1) + 1)] @ compile c1 @
    1.12 - [JMPF (%x. False) (length(compile c2))] @ compile c2"
    1.13 + [JMPF (\<lambda>x. False) (length(compile c2))] @ compile c2"
    1.14  "compile (\<WHILE> b \<DO> c) = [JMPF b (length(compile c) + 1)] @ compile c @
    1.15   [JMPB (length(compile c)+1)]"
    1.16  
    1.17 @@ -68,12 +68,12 @@
    1.18  constdefs
    1.19   forws :: "instr \<Rightarrow> nat set"
    1.20  "forws instr == case instr of
    1.21 - ASIN x a \<Rightarrow> {0} |
    1.22 + SET x a \<Rightarrow> {0} |
    1.23   JMPF b n \<Rightarrow> {0,n} |
    1.24   JMPB n \<Rightarrow> {}"
    1.25   backws :: "instr \<Rightarrow> nat set"
    1.26  "backws instr == case instr of
    1.27 - ASIN x a \<Rightarrow> {} |
    1.28 + SET x a \<Rightarrow> {} |
    1.29   JMPF b n \<Rightarrow> {} |
    1.30   JMPB n \<Rightarrow> {n}"
    1.31  
    1.32 @@ -263,7 +263,7 @@
    1.33        proof cases
    1.34  	assume b: "b s"
    1.35  	then obtain m where m: "n = Suc m"
    1.36 -          and 1: "\<langle>?C @ [?j2],[?j1],s\<rangle> -m\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
    1.37 +          and "\<langle>?C @ [?j2],[?j1],s\<rangle> -m\<rightarrow> \<langle>[],rev ?W,t\<rangle>"
    1.38  	  using H by fastsimp
    1.39  	then obtain r n1 n2 where n1: "\<langle>?C,[],s\<rangle> -n1\<rightarrow> \<langle>[],rev ?C,r\<rangle>"
    1.40            and n2: "\<langle>[?j2],rev ?C @ [?j1],r\<rangle> -n2\<rightarrow> \<langle>[],rev ?W,t\<rangle>"