# HG changeset patch
# User paulson
# Date 968141600 -7200
# Node ID dc84dda48a5a1970e891491c290dd40d779551dd
# Parent  7b26f2d51ba4ebc52b9989c93d79653711636c75
moved proof of "choice" to Tools/meson.ML

diff -r 7b26f2d51ba4 -r dc84dda48a5a src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Tue Sep 05 10:12:48 2000 +0200
+++ b/src/HOL/Fun.ML	Tue Sep 05 10:13:20 2000 +0200
@@ -21,9 +21,7 @@
 
 (** "Axiom" of Choice, proved using the description operator **)
 
-Goal "!!Q. ALL x. EX y. Q x y ==> EX f. ALL x. Q x (f x)";
-by (fast_tac (claset() addEs [selectI]) 1);
-qed "choice";
+(*"choice" is now proved in Tools/meson.ML*)
 
 Goal "!!S. ALL x:S. EX y. Q x y ==> EX f. ALL x:S. Q x (f x)";
 by (fast_tac (claset() addEs [selectI]) 1);