equal
deleted
inserted
replaced
59 Goal "0 ~: A ==> EX f. f: (PROD x:A. x)"; |
59 Goal "0 ~: A ==> EX f. f: (PROD x:A. x)"; |
60 by (rtac AC_Pi 1); |
60 by (rtac AC_Pi 1); |
61 by (REPEAT (ares_tac [non_empty_family] 1)); |
61 by (REPEAT (ares_tac [non_empty_family] 1)); |
62 qed "AC_Pi0"; |
62 qed "AC_Pi0"; |
63 |
63 |
|
64 (*Used in Zorn.ML*) |
|
65 Goal "[| ch : (PROD X:Pow(S) - {0}. X); X<=S; X~=S |] ==> ch ` (S-X) : S-X"; |
|
66 by (etac apply_type 1); |
|
67 by (blast_tac (claset() addSEs [equalityE]) 1); |
|
68 qed "choice_Diff"; |
|
69 |