src/HOL/MicroJava/J/TypeRel.thy
changeset 22597 284b2183d070
parent 22271 51a80e238b29
child 23757 087b0a241557
     1.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Wed Apr 04 23:29:33 2007 +0200
     1.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Wed Apr 04 23:29:37 2007 +0200
     1.3 @@ -150,6 +150,8 @@
     1.4  | subcls         : "G\<turnstile>C\<preceq>C D ==> G\<turnstile>Class C \<preceq> Class D"
     1.5  | null   [intro!]:             "G\<turnstile>     NT \<preceq> RefT R"
     1.6  
     1.7 +lemmas refl = HOL.refl
     1.8 +
     1.9  -- "casting conversion, cf. 5.5 / 5.1.5"
    1.10  -- "left out casts on primitve types"
    1.11  inductive2