src/HOL/MicroJava/J/TypeRel.thy

--- a/src/HOL/MicroJava/J/TypeRel.thy	Wed Apr 04 23:29:33 2007 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.thy	Wed Apr 04 23:29:37 2007 +0200
@@ -150,6 +150,8 @@
 | 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