1.1 --- a/src/HOL/IMP/Compiler.thy	Thu Nov 09 21:38:30 2000 +0100
     1.2 +++ b/src/HOL/IMP/Compiler.thy	Fri Nov 10 09:17:54 2000 +0100
     1.3 @@ -27,7 +27,7 @@
     1.4  ASIN:  "P!n = ASIN x a ==> P |- <s,n> -1-> <s[x::= a s],Suc n>"
     1.5  JMPFT: "[| P!n = JMPF b i;  b s |] ==> P |- <s,n> -1-> <s,Suc n>"
     1.6  JMPFF: "[| P!n = JMPF b i; ~b s; m=n+i |] ==> P |- <s,n> -1-> <s,m>"
     1.7 -JMPB:  "[| P!n = JMB i |] ==> P |- <s,n> -1-> <s,n-i>"
     1.8 +JMPB:  "[| P!n = JMPB i |] ==> P |- <s,n> -1-> <s,n-i>"
     1.9  
    1.10  consts compile :: "com => instr list"
    1.11  primrec