# HG changeset patch
# User nipkow
# Date 973844274 -3600
# Node ID cab4acf9276d83440622166d5191c1f651caa23c
# Parent  17491b8c773271e5ccd1ac106a975f634c3ab5dc
JMB -> JMPB. Email von Johannes Pfeifroth.

diff -r 17491b8c7732 -r cab4acf9276d src/HOL/IMP/Compiler.thy
--- a/src/HOL/IMP/Compiler.thy	Thu Nov 09 21:38:30 2000 +0100
+++ b/src/HOL/IMP/Compiler.thy	Fri Nov 10 09:17:54 2000 +0100
@@ -27,7 +27,7 @@
 ASIN:  "P!n = ASIN x a ==> P |- <s,n> -1-> <s[x::= a s],Suc n>"
 JMPFT: "[| P!n = JMPF b i;  b s |] ==> P |- <s,n> -1-> <s,Suc n>"
 JMPFF: "[| P!n = JMPF b i; ~b s; m=n+i |] ==> P |- <s,n> -1-> <s,m>"
-JMPB:  "[| P!n = JMB i |] ==> P |- <s,n> -1-> <s,n-i>"
+JMPB:  "[| P!n = JMPB i |] ==> P |- <s,n> -1-> <s,n-i>"
 
 consts compile :: "com => instr list"
 primrec