JMB -> JMPB. Email von Johannes Pfeifroth.
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