equal
deleted
inserted
replaced
71 by (Blast_tac 1); |
71 by (Blast_tac 1); |
72 qed "card_M1"; |
72 qed "card_M1"; |
73 |
73 |
74 Goal "\\<exists>x. x\\<in>M1"; |
74 Goal "\\<exists>x. x\\<in>M1"; |
75 by (rtac (card_nonempty RS NotEmpty_ExEl) 1); |
75 by (rtac (card_nonempty RS NotEmpty_ExEl) 1); |
76 by (simp_tac (simpset() addsimps [card_M1, zero_less_prime_power, prime_p]) 1); |
76 by (cut_facts_tac [prime_p RS prime_imp_one_less] 1); |
|
77 by (asm_simp_tac (simpset() addsimps [card_M1]) 1); |
77 qed "exists_x_in_M1"; |
78 qed "exists_x_in_M1"; |
78 |
79 |
79 Goal "M1 <= carrier G"; |
80 Goal "M1 <= carrier G"; |
80 by (rtac (subsetD RS PowD) 1); |
81 by (rtac (subsetD RS PowD) 1); |
81 by (rtac M1_in_M 2); |
82 by (rtac M1_in_M 2); |