equal
deleted
inserted
replaced
428 by (Asm_simp_tac 1); |
428 by (Asm_simp_tac 1); |
429 by (Asm_simp_tac 1); |
429 by (Asm_simp_tac 1); |
430 qed_spec_mp "psubset_card" ; |
430 qed_spec_mp "psubset_card" ; |
431 |
431 |
432 |
432 |
433 (*Relates to equivalence classes. Based on a theorem of F. Kammüller's. |
433 (*Relates to equivalence classes. Based on a theorem of F. Kammueller's. |
434 The "finite C" premise is redundant*) |
434 The "finite C" premise is redundant*) |
435 goal thy "!!C. finite C ==> finite (Union C) --> \ |
435 goal thy "!!C. finite C ==> finite (Union C) --> \ |
436 \ (! c : C. k dvd card c) --> \ |
436 \ (! c : C. k dvd card c) --> \ |
437 \ (! c1: C. ! c2: C. c1 ~= c2 --> c1 Int c2 = {}) \ |
437 \ (! c1: C. ! c2: C. c1 ~= c2 --> c1 Int c2 = {}) \ |
438 \ --> k dvd card(Union C)"; |
438 \ --> k dvd card(Union C)"; |