| changeset 14952 | 47455995693d |
| parent 14171 | 0cab06e3bbd0 |
| child 16417 | 9bc16273c2d4 |
--- a/src/HOL/NanoJava/TypeRel.thy Tue Jun 15 13:24:19 2004 +0200 +++ b/src/HOL/NanoJava/TypeRel.thy Wed Jun 16 14:56:39 2004 +0200 @@ -55,7 +55,8 @@ done lemma subcls1_def2: -"subcls1 = (\<Sigma> C\<in>{C. is_class C} . {D. C\<noteq>Object \<and> super (the (class C)) = D})" + "subcls1 = + (SIGMA C: {C. is_class C} . {D. C\<noteq>Object \<and> super (the (class C)) = D})" apply (unfold subcls1_def is_class_def) apply auto done