src/HOL/MicroJava/JVM/JVMExec.thy

--- a/src/HOL/MicroJava/JVM/JVMExec.thy	Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/JVM/JVMExec.thy	Sun Mar 03 16:59:08 2002 +0100
@@ -34,6 +34,6 @@
 
 syntax (xsymbols)
   exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool"
-              ("_ \<turnstile> _ -jvm-> _" [61,61,61]60)
+              ("_ \<turnstile> _ -jvm\<rightarrow> _" [61,61,61]60)
 
 end