equal
deleted
inserted
replaced
8 theory JVMExec imports JVMExecInstr JVMExceptions begin |
8 theory JVMExec imports JVMExecInstr JVMExceptions begin |
9 |
9 |
10 |
10 |
11 fun |
11 fun |
12 exec :: "jvm_prog \<times> jvm_state => jvm_state option" |
12 exec :: "jvm_prog \<times> jvm_state => jvm_state option" |
13 \<comment> "exec is not recursive. fun is just used for pattern matching" |
13 \<comment> \<open>exec is not recursive. fun is just used for pattern matching\<close> |
14 where |
14 where |
15 "exec (G, xp, hp, []) = None" |
15 "exec (G, xp, hp, []) = None" |
16 |
16 |
17 | "exec (G, None, hp, (stk,loc,C,sig,pc)#frs) = |
17 | "exec (G, None, hp, (stk,loc,C,sig,pc)#frs) = |
18 (let |
18 (let |