src/HOL/MicroJava/J/TypeRel.thy

 where
   refl   [intro!, simp]:       "G\<turnstile>      T \<preceq> T"   -- "identity conv., cf. 5.1.1"
 | subcls         : "G\<turnstile>C\<preceq>C D ==> G\<turnstile>Class C \<preceq> Class D"
 | null   [intro!]:             "G\<turnstile>     NT \<preceq> RefT R"
 
+lemmas refl = HOL.refl
+
 -- "casting conversion, cf. 5.5 / 5.1.5"
 -- "left out casts on primitve types"
 inductive2
   cast    :: "'c prog => [ty   , ty   ] => bool" ("_ \<turnstile> _ \<preceq>? _"  [71,71,71] 70)
   for G :: "'c prog"