src/HOL/MicroJava/BV/Correct.thy

 	 correct_frames G hp phi rT sig frs))))"
 
 
 constdefs
  correct_state :: "[jvm_prog,prog_type,jvm_state] => bool"
-                  ("_,_ \<turnstile>JVM _ \<surd>"  [51,51] 50)
+                  ("_,_ |-JVM _ [ok]"  [51,51] 50)
 "correct_state G phi == \<lambda>(xp,hp,frs).
    case xp of
      None => (case frs of
 	           [] => True
              | (f#fs) => G\<turnstile>h hp\<surd> \<and>

 			 correct_frame G hp s maxl ins f \<and> 
 		         correct_frames G hp phi rT sig fs))
    | Some x => True" 
 
 
-syntax (HTML)
+syntax (xsymbols)
  correct_state :: "[jvm_prog,prog_type,jvm_state] => bool"
-                  ("_,_ |-JVM _ [ok]"  [51,51] 50)
+                  ("_,_ \<turnstile>JVM _ \<surd>"  [51,51] 50)
 
 
 lemma sup_ty_opt_OK:
   "(G \<turnstile> X <=o (OK T')) = (\<exists>T. X = OK T \<and> G \<turnstile> T \<preceq> T')"
   apply (cases X)