changeset 10060 | 4522e59b7d84 |
parent 10057 | 8c8d2d0d3ef8 |
child 10591 | 6d6cb845e841 |
--- a/src/HOL/MicroJava/JVM/JVMExec.thy Fri Sep 22 13:16:24 2000 +0200 +++ b/src/HOL/MicroJava/JVM/JVMExec.thy Fri Sep 22 16:28:04 2000 +0200 @@ -32,7 +32,7 @@ "G \<turnstile> s -jvm-> t == (s,t) \<in> {(s,t). exec(G,s) = Some t}^*" -syntax (HTML output) +syntax (HTML) exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool" ("_ |- _ -jvm-> _" [61,61,61]60)