JMB -> JMPB. Email von Johannes Pfeifroth.
authornipkow
Fri Nov 10 09:17:54 2000 +0100 (2000-11-10)
changeset 10425cab4acf9276d
parent 10424 17491b8c7732
child 10426 469f19c4bf97
JMB -> JMPB. Email von Johannes Pfeifroth.
src/HOL/IMP/Compiler.thy
     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