--- a/src/HOL/MicroJava/BV/JVMType.thy Wed Dec 30 20:24:43 2015 +0100
+++ b/src/HOL/MicroJava/BV/JVMType.thy Wed Dec 30 20:30:42 2015 +0100
@@ -38,29 +38,22 @@
"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))))"