src/HOL/MicroJava/JVM/JVMExecInstr.thy
changeset 10042 7164dc0d24d8
parent 9550 19a6d1289f5e
child 10056 9f84ffa4a8d0
     1.1 --- a/src/HOL/MicroJava/JVM/JVMExecInstr.thy	Wed Sep 20 21:20:41 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/JVM/JVMExecInstr.thy	Thu Sep 21 10:42:49 2000 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  JVMExecInstr = JVMInstructions + JVMState +
     1.5  
     1.6  consts
     1.7 -exec_instr :: "[instr, jvm_prog, aheap, opstack, locvars, cname, sig, p_count, frame list] \\<Rightarrow> jvm_state"
     1.8 +exec_instr :: "[instr, jvm_prog, aheap, opstack, locvars, cname, sig, p_count, frame list] => jvm_state"
     1.9  primrec
    1.10   "exec_instr (Load idx) G hp stk vars Cl sig pc frs = 
    1.11        (None, hp, ((vars ! idx) # stk, vars, Cl, sig, pc+1)#frs)"