
diff -r f56da4769355 -r 4522e59b7d84 src/HOL/MicroJava/BV/Correct.thy
--- a/src/HOL/MicroJava/BV/Correct.thy	Fri Sep 22 13:16:24 2000 +0200
+++ b/src/HOL/MicroJava/BV/Correct.thy	Fri Sep 22 16:28:04 2000 +0200
@@ -55,7 +55,7 @@
 
 constdefs
  correct_state :: "[jvm_prog,prog_type,jvm_state] => bool"
-                  ("_,_\<turnstile>JVM _\<surd>"  [51,51] 50)
+                  ("_,_ \<turnstile>JVM _ \<surd>"  [51,51] 50)
 "correct_state G phi == \<lambda>(xp,hp,frs).
    case xp of
      None => (case frs of
@@ -71,6 +71,11 @@
    | Some x => True" 
 
 
+syntax (HTML)
+ correct_state :: "[jvm_prog,prog_type,jvm_state] => bool"
+                  ("_,_ |-JVM _ [ok]"  [51,51] 50)
+
+
 lemma sup_heap_newref:
   "hp x = None ==> hp \<le>| hp(newref hp \<mapsto> obj)"
 apply (unfold hext_def)




