src/HOL/MicroJava/BV/JVMType.thy

 
 definition  sup :: "'c prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> state binop" where
   "sup S maxs maxr == snd(snd(sl S maxs maxr))"
 
 definition sup_ty_opt :: "['code prog,ty err,ty err] \<Rightarrow> bool"
-                 ("_ |- _ <=o _" [71,71] 70) where 
+                 ("_ \<turnstile> _ <=o _" [71,71] 70) where 
   "sup_ty_opt G == Err.le (subtype G)"
 
 definition sup_loc :: "['code prog,locvars_type,locvars_type] \<Rightarrow> bool" 
-              ("_ |- _ <=l _"  [71,71] 70) where
+              ("_ \<turnstile> _ <=l _"  [71,71] 70) where
   "sup_loc G == Listn.le (sup_ty_opt G)"
 
 definition sup_state :: "['code prog,state_type,state_type] \<Rightarrow> bool"   
-               ("_ |- _ <=s _"  [71,71] 70) where
+               ("_ \<turnstile> _ <=s _"  [71,71] 70) where
   "sup_state G == Product.le (Listn.le (subtype G)) (sup_loc G)"
 
 definition sup_state_opt :: "['code prog,state_type option,state_type option] \<Rightarrow> bool" 
-                   ("_ |- _ <=' _"  [71,71] 70) where
+                   ("_ \<turnstile> _ <=' _"  [71,71] 70) where
   "sup_state_opt G == Opt.le (sup_state G)"
 
-
-notation (xsymbols)
-  sup_ty_opt  ("_ \<turnstile> _ <=o _" [71,71] 70) and
-  sup_loc  ("_ \<turnstile> _ <=l _" [71,71] 70) and
-  sup_state  ("_ \<turnstile> _ <=s _" [71,71] 70) and
-  sup_state_opt  ("_ \<turnstile> _ <=' _" [71,71] 70)
-                   
 
 lemma JVM_states_unfold: 
   "states S maxs maxr == err(opt((\<Union>{list n (types S) |n. n <= maxs}) \<times>
                                   list maxr (err(types S))))"
   apply (unfold states_def sl_def Opt.esl_def Err.sl_def