equal
deleted
inserted
replaced
483 apply (simp add: subcls1_def) |
483 apply (simp add: subcls1_def) |
484 apply auto |
484 apply auto |
485 done |
485 done |
486 |
486 |
487 lemma subint1_def2: |
487 lemma subint1_def2: |
488 "subint1 G = (\<Sigma> I\<in>{I. is_iface G I}. set (isuperIfs (the (iface G I))))" |
488 "subint1 G = (SIGMA I: {I. is_iface G I}. set (isuperIfs (the (iface G I))))" |
489 apply (unfold subint1_def) |
489 apply (unfold subint1_def) |
490 apply auto |
490 apply auto |
491 done |
491 done |
492 |
492 |
493 lemma subcls1_def2: |
493 lemma subcls1_def2: |
494 "subcls1 G = (\<Sigma> C\<in>{C. is_class G C}. {D. C\<noteq>Object \<and> super (the(class G C))=D})" |
494 "subcls1 G = |
|
495 (SIGMA C: {C. is_class G C}. {D. C\<noteq>Object \<and> super (the(class G C))=D})" |
495 apply (unfold subcls1_def) |
496 apply (unfold subcls1_def) |
496 apply auto |
497 apply auto |
497 done |
498 done |
498 |
499 |
499 lemma subcls_is_class: |
500 lemma subcls_is_class: |