src/HOL/MicroJava/J/TypeRel.thy
changeset 18576 8d98b7711e47
parent 18447 da548623916a
child 20970 c2a342e548a9
     1.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Wed Jan 04 17:04:11 2006 +0100
     1.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Wed Jan 04 19:22:53 2006 +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 not_None_eq dest: subcls1D intro: subcls1I)
     1.8 +  by (auto simp add: is_class_def dest: subcls1D intro: subcls1I)
     1.9  
    1.10  lemma finite_subcls1: "finite (subcls1 G)"
    1.11  apply(subst subcls1_def2)