Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
moved proof of "choice" to Tools/meson.ML
authorpaulson
Tue, 05 Sep 2000 10:13:20 +0200
changeset 9838 dc84dda48a5a
parent 9837 7b26f2d51ba4
child 9839 da5ca8b30244
moved proof of "choice" to Tools/meson.ML
src/HOL/Fun.ML file | annotate | diff | comparison | revisions 
--- 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);
isabelle