equal
deleted
inserted
replaced
24 by (asm_simp_tac (simpset() addsimps [image_fun]) 1); |
24 by (asm_simp_tac (simpset() addsimps [image_fun]) 1); |
25 qed "images_eq"; |
25 qed "images_eq"; |
26 |
26 |
27 (* used in \\<in> AC10-AC15.ML AC16WO4.ML WO6WO1.ML *) |
27 (* used in \\<in> AC10-AC15.ML AC16WO4.ML WO6WO1.ML *) |
28 (*I don't know where to put this one.*) |
28 (*I don't know where to put this one.*) |
29 goal Cardinal.thy |
29 Goal |
30 "!!m A B. [| A lepoll succ(m); B \\<subseteq> A; B\\<noteq>0 |] ==> A-B lepoll m"; |
30 "!!m A B. [| A lepoll succ(m); B \\<subseteq> A; B\\<noteq>0 |] ==> A-B lepoll m"; |
31 by (rtac not_emptyE 1 THEN (assume_tac 1)); |
31 by (rtac not_emptyE 1 THEN (assume_tac 1)); |
32 by (ftac singleton_subsetI 1); |
32 by (ftac singleton_subsetI 1); |
33 by (ftac subsetD 1 THEN (assume_tac 1)); |
33 by (ftac subsetD 1 THEN (assume_tac 1)); |
34 by (res_inst_tac [("A2","A")] |
34 by (res_inst_tac [("A2","A")] |
63 (rvimage_id RS subst) 1); |
63 (rvimage_id RS subst) 1); |
64 by (eresolve_tac [id_bij RS bij_ordertype_vimage] 1); |
64 by (eresolve_tac [id_bij RS bij_ordertype_vimage] 1); |
65 qed "ordertype_Int"; |
65 qed "ordertype_Int"; |
66 |
66 |
67 (* used only in AC16_lemmas.ML *) |
67 (* used only in AC16_lemmas.ML *) |
68 goalw CardinalArith.thy [InfCard_def] |
68 Goalw [InfCard_def] |
69 "!!i. [| ~Finite(i); Card(i) |] ==> InfCard(i)"; |
69 "!!i. [| ~Finite(i); Card(i) |] ==> InfCard(i)"; |
70 by (asm_simp_tac (simpset() addsimps [Card_is_Ord RS nat_le_infinite_Ord]) 1); |
70 by (asm_simp_tac (simpset() addsimps [Card_is_Ord RS nat_le_infinite_Ord]) 1); |
71 qed "Inf_Card_is_InfCard"; |
71 qed "Inf_Card_is_InfCard"; |
72 |
72 |
73 Goal "(THE z. {x}={z}) = x"; |
73 Goal "(THE z. {x}={z}) = x"; |