equal
deleted
inserted
replaced
53 apply (unfold subcls1_def) |
53 apply (unfold subcls1_def) |
54 apply auto |
54 apply auto |
55 done |
55 done |
56 |
56 |
57 lemma subcls1_def2: |
57 lemma subcls1_def2: |
58 "subcls1 = (\<Sigma>C\<in>{C. is_class C} . {D. C\<noteq>Object \<and> super (the (class C)) = D})" |
58 "subcls1 = (\<Sigma> C\<in>{C. is_class C} . {D. C\<noteq>Object \<and> super (the (class C)) = D})" |
59 apply (unfold subcls1_def is_class_def) |
59 apply (unfold subcls1_def is_class_def) |
60 apply auto |
60 apply auto |
61 done |
61 done |
62 |
62 |
63 lemma finite_subcls1: "finite subcls1" |
63 lemma finite_subcls1: "finite subcls1" |