src/HOL/MicroJava/JVM/JVMExec.thy
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)