src/HOL/MicroJava/J/TypeRel.thy
changeset 14952 47455995693d
parent 14171 0cab06e3bbd0
child 16417 9bc16273c2d4
     1.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Tue Jun 15 13:24:19 2004 +0200
     1.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Wed Jun 16 14:56:39 2004 +0200
     1.3 @@ -42,7 +42,8 @@
     1.4  done
     1.5  
     1.6  lemma subcls1_def2: 
     1.7 -"subcls1 G = (\<Sigma> C\<in>{C. is_class G C} . {D. C\<noteq>Object \<and> fst (the (class G C))=D})"
     1.8 +  "subcls1 G = 
     1.9 +     (SIGMA C: {C. is_class G C} . {D. C\<noteq>Object \<and> fst (the (class G C))=D})"
    1.10    by (auto simp add: is_class_def dest: subcls1D intro: subcls1I)
    1.11  
    1.12  lemma finite_subcls1: "finite (subcls1 G)"