src/HOL/MicroJava/J/TypeRel.thy
changeset 18447 da548623916a
parent 16417 9bc16273c2d4
child 18576 8d98b7711e47
     1.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Tue Dec 20 22:06:00 2005 +0100
     1.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Wed Dec 21 12:02:57 2005 +0100
     1.3 @@ -44,7 +44,7 @@
     1.4  lemma subcls1_def2: 
     1.5    "subcls1 G = 
     1.6       (SIGMA C: {C. is_class G C} . {D. C\<noteq>Object \<and> fst (the (class G C))=D})"
     1.7 -  by (auto simp add: is_class_def dest: subcls1D intro: subcls1I)
     1.8 +  by (auto simp add: is_class_def not_None_eq dest: subcls1D intro: subcls1I)
     1.9  
    1.10  lemma finite_subcls1: "finite (subcls1 G)"
    1.11  apply(subst subcls1_def2)