diff -r 1d5d181b7e28 -r 648795477bb5 src/HOL/MicroJava/BV/JVMType.thy
--- a/src/HOL/MicroJava/BV/JVMType.thy	Mon Jun 11 19:21:13 2001 +0200
+++ b/src/HOL/MicroJava/BV/JVMType.thy	Tue Jun 12 14:11:00 2001 +0200
@@ -43,31 +43,31 @@
 
 constdefs
   sup_ty_opt :: "['code prog,ty err,ty err] => bool" 
-                 ("_ \<turnstile> _ <=o _" [71,71] 70)
+                 ("_ |- _ <=o _" [71,71] 70)
   "sup_ty_opt G == Err.le (subtype G)"
 
   sup_loc :: "['code prog,locvars_type,locvars_type] => bool" 
-              ("_ \<turnstile> _ <=l _"  [71,71] 70)
+              ("_ |- _ <=l _"  [71,71] 70)
   "sup_loc G == Listn.le (sup_ty_opt G)"
 
   sup_state :: "['code prog,state_type,state_type] => bool"	  
-               ("_ \<turnstile> _ <=s _"  [71,71] 70)
+               ("_ |- _ <=s _"  [71,71] 70)
   "sup_state G == Product.le (Listn.le (subtype G)) (sup_loc G)"
 
   sup_state_opt :: "['code prog,state_type option,state_type option] => bool" 
-                   ("_ \<turnstile> _ <=' _"  [71,71] 70)
+                   ("_ |- _ <=' _"  [71,71] 70)
   "sup_state_opt G == Opt.le (sup_state G)"
 
 
-syntax (HTML) 
+syntax (xsymbols)
   sup_ty_opt    :: "['code prog,ty err,ty err] => bool" 
-                   ("_ |- _ <=o _")
+                   ("_ \<turnstile> _ <=o _" [71,71] 70)
   sup_loc       :: "['code prog,locvars_type,locvars_type] => bool" 
-                   ("_ |- _ <=l _"  [71,71] 70)
+                   ("_ \<turnstile> _ <=l _" [71,71] 70)
   sup_state     :: "['code prog,state_type,state_type] => bool"	
-                   ("_ |- _ <=s _"  [71,71] 70)
+                   ("_ \<turnstile> _ <=s _" [71,71] 70)
   sup_state_opt :: "['code prog,state_type option,state_type option] => bool"
-                   ("_ |- _ <=' _"  [71,71] 70)
+                   ("_ \<turnstile> _ <=' _" [71,71] 70)
                    
 
 lemma JVM_states_unfold: