src/HOL/MicroJava/JVM/JVMExec.thy

   "exec (G, Some xp, hp, frs) = None" 
 
 
 constdefs
   exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool"  
-              ("_ \<turnstile> _ -jvm-> _" [61,61,61]60)
-  "G \<turnstile> s -jvm-> t == (s,t) \<in> {(s,t). exec(G,s) = Some t}^*"
+              ("_ |- _ -jvm-> _" [61,61,61]60)
+  "G |- s -jvm-> t == (s,t) \<in> {(s,t). exec(G,s) = Some t}^*"
 
 
-syntax (HTML)
+syntax (xsymbols)
   exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool"  
-              ("_ |- _ -jvm-> _" [61,61,61]60)
+              ("_ \<turnstile> _ -jvm-> _" [61,61,61]60)
 
 end