src/HOL/Bali/Conform.thy

       objects on the heap are indeed existing classes. Yet this can be 
       inferred for all referenced objs.
 \end{itemize}
 *}
 
-types	env_ = "prog \<times> (lname, ty) table" (* same as env of WellType.thy *)
+types	env' = "prog \<times> (lname, ty) table" (* same as env of WellType.thy *)
 
 
 section "extension of global store"
 
 

 
 section "state conformance"
 
 constdefs
 
-  conforms :: "state \<Rightarrow> env_ \<Rightarrow> bool"          (     "_\<Colon>\<preceq>_"   [71,71]      70)
+  conforms :: "state \<Rightarrow> env' \<Rightarrow> bool"          (     "_\<Colon>\<preceq>_"   [71,71]      70)
    "xs\<Colon>\<preceq>E \<equiv> let (G, L) = E; s = snd xs; l = locals s in
     (\<forall>r. \<forall>obj\<in>globs s r:           G,s\<turnstile>obj   \<Colon>\<preceq>\<surd>r) \<and>
                 \<spacespace>                   G,s\<turnstile>l    [\<sim>\<Colon>\<preceq>]L\<spacespace> \<and>
     (\<forall>a. fst xs=Some(Xcpt (Loc a)) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable)) \<and>
          (fst xs=Some(Jump Ret) \<longrightarrow> l Result \<noteq> None)"