# HG changeset patch
# User wenzelm
# Date 1175722177 -7200
# Node ID 284b2183d070ff780229eaff952c413c5f42ac8b
# Parent  d0d2af4db18f497729b8327e0720508079704498
rebind HOL.refl as refl (hidden by widen.refl);

diff -r d0d2af4db18f -r 284b2183d070 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