diff -r 30693ebd16ae -r 7164dc0d24d8 src/HOL/MicroJava/JVM/JVMExecInstr.thy
--- 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)"