# HG changeset patch
# User paulson
# Date 888574100 -3600
# Node ID 27fa93c22b9b58c7da04001341b0d968e2481556
# Parent  73ba4d19f80246cb093cc8942b4da5dbcfbb7fc0
"choice" moved to Set.ML

diff -r 73ba4d19f802 -r 27fa93c22b9b src/HOL/ex/meson.ML
--- a/src/HOL/ex/meson.ML	Fri Feb 27 11:07:58 1998 +0100
+++ b/src/HOL/ex/meson.ML	Fri Feb 27 11:08:20 1998 +0100
@@ -57,15 +57,6 @@
 val disj_exD2 = prove_fun "P | (? x. Q(x)) ==> ? x. P | Q(x)";
 
 
-(**** Skolemization -- pulling "?" over "!" ****)
-
-(*"Axiom" of Choice, proved using the description operator*)
-val [major] = goal HOL.thy
-    "! x. ? y. Q x y ==> ? f. ! x. Q x (f x)";
-by (cut_facts_tac [major] 1);
-by (fast_tac (claset() addEs [selectI]) 1);
-qed "choice";
-
 
 (***** Generating clauses for the Meson Proof Procedure *****)