--- a/src/HOL/MicroJava/JVM/JVMExecInstr.thy Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/JVM/JVMExecInstr.thy Thu Sep 21 10:42:49 2000 +0200
@@ -9,7 +9,7 @@
JVMExecInstr = JVMInstructions + JVMState +
consts
-exec_instr :: "[instr, jvm_prog, aheap, opstack, locvars, cname, sig, p_count, frame list] \\<Rightarrow> jvm_state"
+exec_instr :: "[instr, jvm_prog, aheap, opstack, locvars, cname, sig, p_count, frame list] => jvm_state"
primrec
"exec_instr (Load idx) G hp stk vars Cl sig pc frs =
(None, hp, ((vars ! idx) # stk, vars, Cl, sig, pc+1)#frs)"