| changeset 67443 | 3abf6a722518 |
| parent 62042 | 6c6ccf573479 |
| child 67613 | ce654b0e6d69 |
--- a/src/HOL/MicroJava/JVM/JVMExec.thy Tue Jan 16 09:12:16 2018 +0100 +++ b/src/HOL/MicroJava/JVM/JVMExec.thy Tue Jan 16 09:30:00 2018 +0100 @@ -10,7 +10,7 @@ fun exec :: "jvm_prog \<times> jvm_state => jvm_state option" -\<comment> "exec is not recursive. fun is just used for pattern matching" +\<comment> \<open>exec is not recursive. fun is just used for pattern matching\<close> where "exec (G, xp, hp, []) = None"