partial restructuring to reduce dependence on Axiom of Choice

--- a/src/HOL/Datatype_Universe.thy	Tue Jul 24 11:25:54 2001 +0200
+++ b/src/HOL/Datatype_Universe.thy	Wed Jul 25 13:13:01 2001 +0200
@@ -9,7 +9,7 @@
 Could <*> be generalized to a general summation (Sigma)?
 *)
 
-Datatype_Universe = NatArith + Sum_Type +
+Datatype_Universe = NatArith + Sum_Type + Hilbert_Choice +
 
 
 (** lists, trees will be sets of nodes **)
@@ -86,10 +86,10 @@
   usum_def   "usum A B == In0`A Un In1`B"
 
   (*the corresponding eliminators*)
-  Split_def  "Split c M == @u. ? x y. M = Scons x y & u = c x y"
+  Split_def  "Split c M == THE u. EX x y. M = Scons x y & u = c x y"
 
-  Case_def   "Case c d M == @u.  (? x . M = In0(x) & u = c(x)) 
-                               | (? y . M = In1(y) & u = d(y))"
+  Case_def   "Case c d M == THE u.  (EX x . M = In0(x) & u = c(x)) 
+                                  | (EX y . M = In1(y) & u = d(y))"
 
 
   (** equality for the "universe" **)

--- a/src/HOL/Finite.ML	Tue Jul 24 11:25:54 2001 +0200
+++ b/src/HOL/Finite.ML	Wed Jul 25 13:13:01 2001 +0200
@@ -333,9 +333,8 @@
 qed "card_empty";
 Addsimps [card_empty];
 
-Goal "x ~: A ==> \
-\     ((insert x A, n) : cardR) =  \
-\     (EX m. (A, m) : cardR & n = Suc m)";
+Goal "x ~: A \
+\     ==> ((insert x A, n) : cardR)  =  (EX m. (A, m) : cardR & n = Suc m)";
 by Auto_tac;
 by (res_inst_tac [("A1", "A")] (finite_imp_cardR RS exE) 1);
 by (force_tac (claset() addDs [cardR_imp_finite], simpset()) 1);
@@ -345,7 +344,7 @@
 Goalw [card_def]
      "[| finite A; x ~: A |] ==> card (insert x A) = Suc(card A)";
 by (asm_simp_tac (simpset() addsimps [lemma]) 1);
-by (rtac some_equality 1);
+by (rtac the_equality 1);
 by (auto_tac (claset() addIs [finite_imp_cardR],
 	      simpset() addcongs [conj_cong]
 		        addsimps [symmetric card_def,
@@ -624,7 +623,7 @@
 Goalw [fold_def]
      "[| finite A; x ~: A |] ==> fold f e (insert x A) = f x (fold f e A)";
 by (asm_simp_tac (simpset() addsimps [lemma]) 1);
-by (rtac some_equality 1);
+by (rtac the_equality 1);
 by (auto_tac (claset() addIs [finite_imp_foldSet],
 	      simpset() addcongs [conj_cong]
 		        addsimps [symmetric fold_def,

--- a/src/HOL/Finite.thy	Tue Jul 24 11:25:54 2001 +0200
+++ b/src/HOL/Finite.thy	Wed Jul 25 13:13:01 2001 +0200
@@ -37,7 +37,7 @@
 
 constdefs
   card :: 'a set => nat
- "card A == @n. (A,n) : cardR"
+ "card A == THE n. (A,n) : cardR"
 
 (*
 A "fold" functional for finite sets.  For n non-negative we have
@@ -56,7 +56,7 @@
 
 constdefs
    fold :: "[['b,'a] => 'a, 'a, 'b set] => 'a"
-  "fold f e A == @x. (A,x) : foldSet f e"
+  "fold f e A == THE x. (A,x) : foldSet f e"
 
    setsum :: "('a => 'b) => 'a set => ('b::{plus, zero})"
   "setsum f A == if finite A then fold (op+ o f) 0 A else 0"

--- a/src/HOL/Fun.ML	Tue Jul 24 11:25:54 2001 +0200
+++ b/src/HOL/Fun.ML	Wed Jul 25 13:13:01 2001 +0200
@@ -19,15 +19,6 @@
 qed "apply_inverse";
 
 
-(** "Axiom" of Choice, proved using the description operator **)
-
-(*"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 [someI]) 1);
-qed "bchoice";
-
-
 section "id";
 
 Goalw [id_def] "id x = x";
@@ -35,11 +26,6 @@
 qed "id_apply";
 Addsimps [id_apply];
 
-Goal "inv id = id";
-by (simp_tac (simpset() addsimps [inv_def,id_def]) 1);
-qed "inv_id";
-Addsimps [inv_id];
-
 
 section "o";
 
@@ -113,28 +99,6 @@
 by (assume_tac 1);
 qed "inj_eq";
 
-(*A one-to-one function has an inverse (given using select).*)
-Goalw [inv_def] "inj(f) ==> inv f (f x) = x";
-by (asm_simp_tac (simpset() addsimps [inj_eq]) 1); 
-qed "inv_f_f";
-Addsimps [inv_f_f];
-
-Goal "[| inj(f);  f x = y |] ==> inv f y = x";
-by (etac subst 1);
-by (etac inv_f_f 1);
-qed "inv_f_eq";
-
-Goal "[| inj f; ALL x. f(g x) = x |] ==> inv f = g";
-by (blast_tac (claset() addIs [ext, inv_f_eq]) 1); 
-qed "inj_imp_inv_eq";
-
-(* Useful??? *)
-val [oneone,minor] = Goal
-    "[| inj(f); !!y. y: range(f) ==> P(inv f y) |] ==> P(x)";
-by (res_inst_tac [("t", "x")] (oneone RS (inv_f_f RS subst)) 1);
-by (rtac (rangeI RS minor) 1);
-qed "inj_transfer";
-
 Goalw [o_def] "[| inj f; f o g = f o h |] ==> g = h";
 by (rtac ext 1);
 by (etac injD 1);
@@ -157,11 +121,6 @@
 qed "inj_on_inverseI";
 bind_thm ("inj_inverseI", inj_on_inverseI);   (*for compatibility*)
 
-Goal "(inj f) = (inv f o f = id)";
-by (asm_simp_tac (simpset() addsimps [o_def, expand_fun_eq]) 1);
-by (blast_tac (claset() addIs [inj_inverseI, inv_f_f]) 1);
-qed "inj_iff";
-
 Goalw [inj_on_def] "[| inj_on f A;  f(x)=f(y);  x:A;  y:A |] ==> x=y";
 by (Blast_tac 1);
 qed "inj_onD";
@@ -170,6 +129,10 @@
 by (blast_tac (claset() addSDs [inj_onD]) 1);
 qed "inj_on_iff";
 
+Goalw [o_def] "[| inj_on f A;  inj_on g (f`A) |] ==> inj_on (g o f) A";
+by (fast_tac (claset() addIs [inj_onI] addEs [inj_onD]) 1);
+qed "comp_inj_on";
+
 Goalw [inj_on_def] "[| inj_on f A;  ~x=y;  x:A;  y:A |] ==> ~ f(x)=f(y)";
 by (Blast_tac 1);
 qed "inj_on_contraD";
@@ -198,49 +161,6 @@
 by (Blast_tac 1);
 qed "surjD";
 
-Goal "inj f ==> surj (inv f)";
-by (blast_tac (claset() addIs [surjI, inv_f_f]) 1);
-qed "inj_imp_surj_inv";
-
-
-(*** Lemmas about injective functions and inv ***)
-
-Goalw [o_def] "[| inj_on f A;  inj_on g (f`A) |] ==> inj_on (g o f) A";
-by (fast_tac (claset() addIs [inj_onI] addEs [inj_onD]) 1);
-qed "comp_inj_on";
-
-Goalw [inv_def] "y : range(f) ==> f(inv f y) = y";
-by (fast_tac (claset() addIs [someI]) 1);
-qed "f_inv_f";
-
-Goal "surj f ==> f(inv f y) = y";
-by (asm_simp_tac (simpset() addsimps [f_inv_f, surj_range]) 1);
-qed "surj_f_inv_f";
-
-Goal "[| inv f x = inv f y;  x: range(f);  y: range(f) |] ==> x=y";
-by (rtac (arg_cong RS box_equals) 1);
-by (REPEAT (ares_tac [f_inv_f] 1));
-qed "inv_injective";
-
-Goal "A <= range(f) ==> inj_on (inv f) A";
-by (fast_tac (claset() addIs [inj_onI] 
-                       addEs [inv_injective, injD]) 1);
-qed "inj_on_inv";
-
-Goal "surj f ==> inj (inv f)";
-by (asm_simp_tac (simpset() addsimps [inj_on_inv, surj_range]) 1);
-qed "surj_imp_inj_inv";
-
-Goal "(surj f) = (f o inv f = id)";
-by (asm_simp_tac (simpset() addsimps [o_def, expand_fun_eq]) 1);
-by (blast_tac (claset() addIs [surjI, surj_f_inv_f]) 1);
-qed "surj_iff";
-
-Goal "[| surj f; ALL x. g(f x) = x |] ==> inv f = g";
-by (rtac ext 1);
-by (dres_inst_tac [("x","inv f x")] spec 1); 
-by (asm_full_simp_tac (simpset() addsimps [surj_f_inv_f]) 1); 
-qed "surj_imp_inv_eq";
 
 
 (** Bijections **)
@@ -257,33 +177,6 @@
 by (Blast_tac 1);
 qed "bij_is_surj";
 
-Goalw [bij_def] "bij f ==> bij (inv f)";
-by (asm_simp_tac (simpset() addsimps [inj_imp_surj_inv, surj_imp_inj_inv]) 1);
-qed "bij_imp_bij_inv";
-
-val prems = 
-Goalw [inv_def] "[| !! x. g (f x) = x;  !! y. f (g y) = y |] ==> inv f = g";
-by (rtac ext 1);
-by (auto_tac (claset(), simpset() addsimps prems));
-qed "inv_equality";
-
-Goalw [bij_def] "bij f ==> inv (inv f) = f";
-by (rtac inv_equality 1);
-by (auto_tac (claset(), simpset() addsimps [surj_f_inv_f]));
-qed "inv_inv_eq";
-
-(** bij(inv f) implies little about f.  Consider f::bool=>bool such that
-    f(True)=f(False)=True.  Then it's consistent with axiom someI that
-    inv(f) could be any function at all, including the identity function.
-    If inv(f)=id then inv(f) is a bijection, but inj(f), surj(f) and
-    inv(inv(f))=f all fail.
-**)
-
-Goalw [bij_def] "[| bij f; bij g |] ==> inv (f o g) = inv g o inv f";
-by (rtac (inv_equality) 1);
-by (auto_tac (claset(), simpset() addsimps [surj_f_inv_f]));
-qed "o_inv_distrib";
-
 
 (** We seem to need both the id-forms and the (%x. x) forms; the latter can
     arise by rewriting, while id may be used explicitly. **)
@@ -323,18 +216,10 @@
 by (asm_simp_tac (simpset() addsimps [surj_range]) 1);
 qed "surj_image_vimage_eq";
 
-Goal "surj f ==> f ` (inv f ` A) = A";
-by (asm_simp_tac (simpset() addsimps [image_eq_UN, surj_f_inv_f]) 1);
-qed "image_surj_f_inv_f";
-
 Goalw [inj_on_def] "inj f ==> f -` (f ` A) = A";
 by (Blast_tac 1);
 qed "inj_vimage_image_eq";
 
-Goal "inj f ==> (inv f) ` (f ` A) = A";
-by (asm_simp_tac (simpset() addsimps [image_eq_UN]) 1);
-qed "image_inv_f_f";
-
 Goalw [surj_def] "surj f ==> f -` B <= A ==> B <= f ` A";
 by (blast_tac (claset() addIs [sym]) 1);
 qed "vimage_subsetD";
@@ -374,10 +259,6 @@
 by (Blast_tac 1);
 qed "image_set_diff";
 
-Goalw [image_def] "inj(f) ==> inv(f)`(f`X) = X";
-by Auto_tac;
-qed "inv_image_comp";
-
 Goal "inj f ==> (f a : f`A) = (a : A)";
 by (blast_tac (claset() addDs [injD]) 1);
 qed "inj_image_mem_iff";
@@ -404,22 +285,10 @@
 (*Compare with image_INT: no use of inj_on, and if f is surjective then
   it doesn't matter whether A is empty*)
 Goalw [bij_def] "bij f ==> f ` (INTER A B) = (INT x:A. f ` B x)";
-by (force_tac (claset() addSIs [surj_f_inv_f RS sym RS image_eqI], 
-	       simpset()) 1);
+by (asm_full_simp_tac (simpset() addsimps [inj_on_def, surj_def]) 1);
+by (Blast_tac 1);  
 qed "bij_image_INT";
 
-Goal "bij f ==> f ` Collect P = {y. P (inv f y)}";
-by Auto_tac;
-by (force_tac (claset(), simpset() addsimps [bij_is_inj]) 1);
-by (blast_tac (claset() addIs [bij_is_surj RS surj_f_inv_f RS sym]) 1);
-qed "bij_image_Collect_eq";
-
-Goal "bij f ==> f -` A = inv f ` A";
-by Safe_tac;
-by (asm_simp_tac (simpset() addsimps [bij_is_surj RS surj_f_inv_f]) 2);
-by (blast_tac (claset() addIs [bij_is_inj RS inv_f_f RS sym]) 1);
-qed "bij_vimage_eq_inv_image";
-
 Goal "surj f ==> -(f`A) <= f`(-A)";
 by (auto_tac (claset(), simpset() addsimps [surj_def]));  
 qed "surj_Compl_image_subset";
@@ -504,13 +373,13 @@
 (*** -> and Pi, by Florian Kammueller and LCP ***)
 
 val prems = Goalw [Pi_def]
-"[| !!x. x: A ==> f x: B x; !!x. x ~: A  ==> f(x) = (@ y. True)|] \
+"[| !!x. x: A ==> f x: B x; !!x. x ~: A  ==> f(x) = arbitrary|] \
 \    ==> f: Pi A B";
 by (auto_tac (claset(), simpset() addsimps prems));
 qed "Pi_I";
 
 val prems = Goal 
-"[| !!x. x: A ==> f x: B; !!x. x ~: A  ==> f(x) = (@ y. True)|] ==> f: A funcset B";
+"[| !!x. x: A ==> f x: B; !!x. x ~: A  ==> f(x) = arbitrary|] ==> f: A funcset B";
 by (blast_tac (claset() addIs Pi_I::prems) 1);
 qed "funcsetI";
 
@@ -522,7 +391,7 @@
 by Auto_tac;
 qed "funcset_mem";
 
-Goalw [Pi_def] "[|f: Pi A B; x~: A|] ==> f x = (@ y. True)";
+Goalw [Pi_def] "[|f: Pi A B; x~: A|] ==> f x = arbitrary";
 by Auto_tac;
 qed "apply_arb";
 
@@ -573,7 +442,7 @@
 by (asm_simp_tac (simpset() addsimps prems) 1);
 qed "restrictI";
 
-Goal "(lam y: A. f y) x = (if x : A then f x else (@ y. True))";
+Goal "(lam y: A. f y) x = (if x : A then f x else arbitrary)";
 by (asm_simp_tac (simpset() addsimps [restrict_def]) 1);
 qed "restrict_apply";
 Addsimps [restrict_apply];
@@ -590,32 +459,6 @@
 qed "inj_on_restrict_eq";
 
 
-(*** Inverse ***)
-
-Goalw [Inv_def] "f ` A = B ==> (lam x: B. (Inv A f) x) : B funcset A";
-by (fast_tac (claset() addIs [restrict_in_funcset, someI2]) 1);
-qed "Inv_funcset";
-
-Goal "[| inj_on f A;  x : A |] ==> Inv A f (f x) = x";
-by (asm_full_simp_tac (simpset() addsimps [Inv_def, inj_on_def]) 1);
-by (blast_tac (claset() addIs [someI2]) 1); 
-qed "Inv_f_f";
-
-Goal "y : f`A  ==> f (Inv A f y) = y";
-by (asm_simp_tac (simpset() addsimps [Inv_def]) 1);
-by (fast_tac (claset() addIs [someI2]) 1);
-qed "f_Inv_f";
-
-Goal "[| Inv A f x = Inv A f y;  x : f`A;  y : f`A |] ==> x=y";
-by (rtac (arg_cong RS box_equals) 1);
-by (REPEAT (ares_tac [f_Inv_f] 1));
-qed "Inv_injective";
-
-Goal "B <= f`A ==> inj_on (Inv A f) B";
-by (rtac inj_onI 1);
-by (blast_tac (claset() addIs [inj_onI] addDs [Inv_injective, injD]) 1);
-qed "inj_on_Inv";
-
 Goal "f : A funcset B ==> compose A (lam y:B. y) f = f";
 by (rtac ext 1); 
 by (auto_tac (claset(), simpset() addsimps [compose_def, Pi_def])); 
@@ -626,15 +469,6 @@
 by (auto_tac (claset(), simpset() addsimps [compose_def, Pi_def])); 
 qed "compose_Id";
 
-Goal "[| inj_on f A;  f ` A = B |] \
-\     ==> compose A (lam y:B. (Inv A f) y) f = (lam x: A. x)";
-by (asm_simp_tac (simpset() addsimps [compose_def]) 1);
-by (rtac restrict_ext 1); 
-by Auto_tac; 
-by (etac subst 1); 
-by (asm_full_simp_tac (simpset() addsimps [Inv_f_f]) 1);
-qed "compose_Inv_id";
-
 
 (*** Pi ***)
 
@@ -646,7 +480,7 @@
 by (blast_tac (HOL_cs addIs [Pi_eq_empty]) 1);
 qed "Pi_total1";
 
-Goal "Pi {} B = { %x. @y. True }";
+Goal "Pi {} B = { %x. arbitrary }";
 by (auto_tac (claset() addIs [ext], simpset() addsimps [Pi_def]));
 qed "Pi_empty";
 

--- a/src/HOL/Fun.thy	Tue Jul 24 11:25:54 2001 +0200
+++ b/src/HOL/Fun.thy	Wed Jul 25 13:13:01 2001 +0200
@@ -43,9 +43,6 @@
   o  :: ['b => 'c, 'a => 'b, 'a] => 'c   (infixl 55)
     "f o g == %x. f(g(x))"
 
-  inv :: ('a => 'b) => ('b => 'a)
-    "inv(f::'a=>'b) == % y. @x. f(x)=y"
-
   inj_on :: ['a => 'b, 'a set] => bool
     "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y"
 
@@ -70,17 +67,20 @@
   
 constdefs
   Pi      :: "['a set, 'a => 'b set] => ('a => 'b) set"
-    "Pi A B == {f. ! x. if x:A then f(x) : B(x) else f(x) = (@ y. True)}"
+    "Pi A B == {f. ! x. if x:A then f(x) : B(x) else f(x) = arbitrary}"
 
   restrict :: "['a => 'b, 'a set] => ('a => 'b)"
-    "restrict f A == (%x. if x : A then f x else (@ y. True))"
+    "restrict f A == (%x. if x : A then f x else arbitrary)"
 
 syntax
-  "@Pi"  :: "[idt, 'a set, 'b set] => ('a => 'b) set"  ("(3PI _:_./ _)" 10)
+  "@Pi"  :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3PI _:_./ _)" 10)
   funcset :: "['a set, 'b set] => ('a => 'b) set"      (infixr 60) 
   "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a => 'b)"  ("(3lam _:_./ _)" 10)
 
-  (*Giving funcset the nice arrow syntax -> clashes with existing theories*)
+  (*Giving funcset the arrow syntax (namely ->) clashes with other theories*)
+
+syntax (symbols)
+  "@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\\<Pi> _\\<in>_./ _)"   10)
 
 translations
   "PI x:A. B" => "Pi A (%x. B)"
@@ -91,8 +91,6 @@
   compose :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)"
     "compose A g f == lam x : A. g(f x)"
 
-  Inv    :: "['a set, 'a => 'b] => ('b => 'a)"
-    "Inv A f == (% x. (@ y. y : A & f y = x))"
 
   
 end

--- a/src/HOL/GroupTheory/Bij.thy	Tue Jul 24 11:25:54 2001 +0200
+++ b/src/HOL/GroupTheory/Bij.thy	Wed Jul 25 13:13:01 2001 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/GroupTheory/Coset
+(*  Title:      HOL/GroupTheory/Bij
     ID:         $Id$
     Author:     Florian Kammueller, with new proofs by L C Paulson
     Copyright   1998-2001  University of Cambridge

--- a/src/HOL/GroupTheory/Ring.thy	Tue Jul 24 11:25:54 2001 +0200
+++ b/src/HOL/GroupTheory/Ring.thy	Wed Jul 25 13:13:01 2001 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/GroupTheory/Bij
+(*  Title:      HOL/GroupTheory/Ring
     ID:         $Id$
     Author:     Florian Kammueller, with new proofs by L C Paulson
     Copyright   1998-2001  University of Cambridge

--- a/src/HOL/HOL.ML	Tue Jul 24 11:25:54 2001 +0200
+++ b/src/HOL/HOL.ML	Wed Jul 25 13:13:01 2001 +0200
@@ -12,7 +12,6 @@
   val refl = refl;
   val subst = subst;
   val ext = ext;
-  val someI = someI;
   val impI = impI;
   val mp = mp;
   val True_def = True_def;
@@ -31,6 +30,6 @@
 end;
 
 AddXIs [equal_intr_rule, disjI1, disjI2, ext];
-AddXEs [ex1_implies_ex, someI_ex, sym];
+AddXEs [ex1_implies_ex, sym];
 
 open HOL;

--- a/src/HOL/HOL.thy	Tue Jul 24 11:25:54 2001 +0200
+++ b/src/HOL/HOL.thy	Wed Jul 25 13:13:01 2001 +0200
@@ -7,8 +7,7 @@
 *)
 
 theory HOL = CPure
-files ("HOL_lemmas.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML")
-  ("meson_lemmas.ML") ("Tools/meson.ML"):
+files ("HOL_lemmas.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML"):
 
 
 (** Core syntax **)
@@ -37,7 +36,6 @@
 
   (* Binders *)
 
-  Eps           :: "('a => bool) => 'a"
   The           :: "('a => bool) => 'a"
   All           :: "('a => bool) => bool"           (binder "ALL " 10)
   Ex            :: "('a => bool) => bool"           (binder "EX " 10)
@@ -79,9 +77,9 @@
   divide        :: "['a::inverse, 'a] => 'a"        (infixl "'/" 70)
 
 syntax (xsymbols)
-  abs :: "'a::minus => 'a"    ("\<bar>_\<bar>")
+  abs :: "'a::minus => 'a"    ("\\<bar>_\\<bar>")
 syntax (HTML output)
-  abs :: "'a::minus => 'a"    ("\<bar>_\<bar>")
+  abs :: "'a::minus => 'a"    ("\\<bar>_\\<bar>")
 
 axclass plus_ac0 < plus, zero
   commute: "x + y = y + x"
@@ -97,7 +95,6 @@
 
 syntax
   ~=            :: "['a, 'a] => bool"                    (infixl 50)
-  "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3SOME _./ _)" [0, 10] 10)
   "_The"        :: "[pttrn, bool] => 'a"                 ("(3THE _./ _)" [0, 10] 10)
 
   (* Let expressions *)
@@ -116,7 +113,6 @@
 
 translations
   "x ~= y"                == "~ (x = y)"
-  "SOME x. P"             == "Eps (%x. P)"
   "THE x. P"              == "The (%x. P)"
   "_Let (_binds b bs) e"  == "_Let b (_Let bs e)"
   "let x = a in e"        == "Let a (%x. e)"
@@ -126,31 +122,27 @@
   "op ~="       :: "['a, 'a] => bool"                    ("(_ ~=/ _)" [51, 51] 50)
 
 syntax (symbols)
-  Not           :: "bool => bool"                        ("\<not> _" [40] 40)
-  "op &"        :: "[bool, bool] => bool"                (infixr "\<and>" 35)
-  "op |"        :: "[bool, bool] => bool"                (infixr "\<or>" 30)
-  "op -->"      :: "[bool, bool] => bool"                (infixr "\<midarrow>\<rightarrow>" 25)
-  "op ~="       :: "['a, 'a] => bool"                    (infixl "\<noteq>" 50)
-  "ALL "        :: "[idts, bool] => bool"                ("(3\<forall>_./ _)" [0, 10] 10)
-  "EX "         :: "[idts, bool] => bool"                ("(3\<exists>_./ _)" [0, 10] 10)
-  "EX! "        :: "[idts, bool] => bool"                ("(3\<exists>!_./ _)" [0, 10] 10)
-  "_case1"      :: "['a, 'b] => case_syn"                ("(2_ \<Rightarrow>/ _)" 10)
+  Not           :: "bool => bool"                        ("\\<not> _" [40] 40)
+  "op &"        :: "[bool, bool] => bool"                (infixr "\\<and>" 35)
+  "op |"        :: "[bool, bool] => bool"                (infixr "\\<or>" 30)
+  "op -->"      :: "[bool, bool] => bool"                (infixr "\\<midarrow>\\<rightarrow>" 25)
+  "op ~="       :: "['a, 'a] => bool"                    (infixl "\\<noteq>" 50)
+  "ALL "        :: "[idts, bool] => bool"                ("(3\\<forall>_./ _)" [0, 10] 10)
+  "EX "         :: "[idts, bool] => bool"                ("(3\\<exists>_./ _)" [0, 10] 10)
+  "EX! "        :: "[idts, bool] => bool"                ("(3\\<exists>!_./ _)" [0, 10] 10)
+  "_case1"      :: "['a, 'b] => case_syn"                ("(2_ \\<Rightarrow>/ _)" 10)
 (*"_case2"      :: "[case_syn, cases_syn] => cases_syn"  ("_/ \\<orelse> _")*)
 
-syntax (input)
-  "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3\<epsilon>_./ _)" [0, 10] 10)
-
 syntax (symbols output)
-  "op ~="       :: "['a, 'a] => bool"                    ("(_ \<noteq>/ _)" [51, 51] 50)
+  "op ~="       :: "['a, 'a] => bool"                    ("(_ \\<noteq>/ _)" [51, 51] 50)
 
 syntax (xsymbols)
-  "op -->"      :: "[bool, bool] => bool"                (infixr "\<longrightarrow>" 25)
+  "op -->"      :: "[bool, bool] => bool"                (infixr "\\<longrightarrow>" 25)
 
 syntax (HTML output)
-  Not           :: "bool => bool"                        ("\<not> _" [40] 40)
+  Not           :: "bool => bool"                        ("\\<not> _" [40] 40)
 
 syntax (HOL)
-  "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3@ _./ _)" [0, 10] 10)
   "ALL "        :: "[idts, bool] => bool"                ("(3! _./ _)" [0, 10] 10)
   "EX "         :: "[idts, bool] => bool"                ("(3? _./ _)" [0, 10] 10)
   "EX! "        :: "[idts, bool] => bool"                ("(3?! _./ _)" [0, 10] 10)
@@ -173,7 +165,6 @@
     rule, and similar to the ABS rule of HOL.*)
   ext:          "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)"
 
-  someI:        "P (x::'a) ==> P (SOME x. P x)"
   the_eq_trivial: "(THE x. x = a) = (a::'a)"
 
   impI:         "(P ==> Q) ==> P-->Q"
@@ -183,7 +174,7 @@
 
   True_def:     "True      == ((%x::bool. x) = (%x. x))"
   All_def:      "All(P)    == (P = (%x. True))"
-  Ex_def:       "Ex(P)     == P (SOME x. P x)"
+  Ex_def:       "Ex(P)     == !Q. (!x. P x --> Q) --> Q"
   False_def:    "False     == (!P. P)"
   not_def:      "~ P       == P-->False"
   and_def:      "P & Q     == !R. (P-->Q-->R) --> R"
@@ -199,11 +190,11 @@
 defs
   (*misc definitions*)
   Let_def:      "Let s f == f(s)"
-  if_def:       "If P x y == SOME z::'a. (P=True --> z=x) & (P=False --> z=y)"
+  if_def:       "If P x y == THE z::'a. (P=True --> z=x) & (P=False --> z=y)"
 
   (*arbitrary is completely unspecified, but is made to appear as a
     definition syntactically*)
-  arbitrary_def:  "False ==> arbitrary == (SOME x. False)"
+  arbitrary_def:  "False ==> arbitrary == (THE x. False)"
 
 
 
@@ -256,8 +247,4 @@
 setup "Simplifier.method_setup Splitter.split_modifiers" setup simpsetup
 setup Splitter.setup setup Clasimp.setup
 
-use "meson_lemmas.ML"
-use "Tools/meson.ML"
-setup meson_setup
-
 end

--- a/src/HOL/HOL_lemmas.ML	Tue Jul 24 11:25:54 2001 +0200
+++ b/src/HOL/HOL_lemmas.ML	Wed Jul 25 13:13:01 2001 +0200
@@ -15,7 +15,6 @@
 val refl = thm "refl";
 val subst = thm "subst";
 val ext = thm "ext";
-val someI = thm "someI";
 val impI = thm "impI";
 val mp = thm "mp";
 val True_def = thm "True_def";
@@ -222,12 +221,18 @@
 section "Existential quantifier";
 
 Goalw [Ex_def] "P x ==> EX x::'a. P x";
-by (etac someI 1) ;
+by (rtac allI 1); 
+by (rtac impI 1); 
+by (etac allE 1); 
+by (etac mp 1) ;
+by (assume_tac 1); 
 qed "exI";
 
 val [major,minor] =
 Goalw [Ex_def] "[| EX x::'a. P(x); !!x. P(x) ==> Q |] ==> Q";
-by (rtac (major RS minor) 1);
+by (rtac (major RS spec RS mp) 1); 
+by (rtac (impI RS allI) 1); 
+by (etac minor 1); 
 qed "exE";
 
 
@@ -344,66 +349,6 @@
 qed "ex1_implies_ex";
 
 
-section "SOME: Hilbert's Epsilon-operator";
-
-(*Easier to apply than someI if witness ?a comes from an EX-formula*)
-Goal "EX x. P x ==> P (SOME x. P x)";
-by (etac exE 1);
-by (etac someI 1);
-qed "someI_ex";
-
-(*Easier to apply than someI: conclusion has only one occurrence of P*)
-val prems = Goal "[| P a;  !!x. P x ==> Q x |] ==> Q (SOME x. P x)";
-by (resolve_tac prems 1);
-by (rtac someI 1);
-by (resolve_tac prems 1) ;
-qed "someI2";
-
-(*Easier to apply than someI2 if witness ?a comes from an EX-formula*)
-val [major,minor] = Goal "[| EX a. P a; !!x. P x ==> Q x |] ==> Q (SOME x. P x)";
-by (rtac (major RS exE) 1);
-by (etac someI2 1 THEN etac minor 1);
-qed "someI2_ex";
-
-val prems = Goal "[| P a;  !!x. P x ==> x=a |] ==> (SOME x. P x) = a";
-by (rtac someI2 1);
-by (REPEAT (ares_tac prems 1)) ;
-qed "some_equality";
-
-Goal "[| EX!x. P x; P a |] ==> (SOME x. P x) = a";
-by (rtac some_equality 1);
-by  (atac 1);
-by (etac ex1E 1);
-by (etac all_dupE 1);
-by (dtac mp 1);
-by  (atac 1);
-by (etac ssubst 1);
-by (etac allE 1);
-by (etac mp 1);
-by (atac 1);
-qed "some1_equality";
-
-Goal "P (SOME x. P x) =  (EX x. P x)";
-by (rtac iffI 1);
-by (etac exI 1);
-by (etac exE 1);
-by (etac someI 1);
-qed "some_eq_ex";
-
-Goal "(SOME y. y=x) = x";
-by (rtac some_equality 1);
-by (rtac refl 1);
-by (atac 1);
-qed "some_eq_trivial";
-
-Goal "(SOME y. x=y) = x";
-by (rtac some_equality 1);
-by (rtac refl 1);
-by (etac sym 1);
-qed "some_sym_eq_trivial";
-
-
-
 section "THE: definite description operator";
 
 val [prema,premx] = Goal "[| P a;  !!x. P x ==> x=a |] ==> (THE x. P x) = a";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hilbert_Choice.thy	Wed Jul 25 13:13:01 2001 +0200
@@ -0,0 +1,187 @@
+(*  Title:      HOL/Hilbert_Choice.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson
+    Copyright   2001  University of Cambridge
+
+Hilbert's epsilon-operator and everything to do with the Axiom of Choice
+*)
+
+theory Hilbert_Choice = NatArith
+files ("Hilbert_Choice_lemmas.ML") ("meson_lemmas.ML") ("Tools/meson.ML"):
+
+consts
+  Eps           :: "('a => bool) => 'a"
+
+
+syntax (input)
+  "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3\\<epsilon>_./ _)" [0, 10] 10)
+
+syntax (HOL)
+  "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3@ _./ _)" [0, 10] 10)
+
+syntax
+  "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3SOME _./ _)" [0, 10] 10)
+
+translations
+  "SOME x. P"             == "Eps (%x. P)"
+
+axioms  
+  someI:        "P (x::'a) ==> P (SOME x. P x)"
+
+
+constdefs  
+  inv :: "('a => 'b) => ('b => 'a)"
+    "inv(f::'a=>'b) == % y. @x. f(x)=y"
+
+  Inv :: "['a set, 'a => 'b] => ('b => 'a)"
+    "Inv A f == (% x. (@ y. y : A & f y = x))"
+
+
+use "Hilbert_Choice_lemmas.ML"
+
+
+(** Least value operator **)
+
+constdefs
+  LeastM   :: "['a => 'b::ord, 'a => bool] => 'a"
+              "LeastM m P == @x. P x & (ALL y. P y --> m x <= m y)"
+
+syntax
+ "@LeastM" :: "[pttrn, 'a=>'b::ord, bool] => 'a" ("LEAST _ WRT _. _" [0,4,10]10)
+
+translations
+                "LEAST x WRT m. P" == "LeastM m (%x. P)"
+
+lemma LeastMI2:
+  "[| P x; !!y. P y ==> m x <= m y;
+           !!x. [| P x; \\<forall>y. P y --> m x \\<le> m y |] ==> Q x |]
+   ==> Q (LeastM m P)";
+apply (unfold LeastM_def)
+apply (rule someI2_ex)
+apply  blast
+apply blast
+done
+
+lemma LeastM_equality:
+ "[| P k; !!x. P x ==> m k <= m x |] ==> m (LEAST x WRT m. P x) = 
+     (m k::'a::order)";
+apply (rule LeastMI2)
+apply   assumption
+apply  blast
+apply (blast intro!: order_antisym) 
+done
+
+
+(** Greatest value operator **)
+
+constdefs
+  GreatestM   :: "['a => 'b::ord, 'a => bool] => 'a"
+              "GreatestM m P == @x. P x & (ALL y. P y --> m y <= m x)"
+  
+  Greatest    :: "('a::ord => bool) => 'a"         (binder "GREATEST " 10)
+              "Greatest     == GreatestM (%x. x)"
+
+syntax
+ "@GreatestM" :: "[pttrn, 'a=>'b::ord, bool] => 'a"
+                                        ("GREATEST _ WRT _. _" [0,4,10]10)
+
+translations
+              "GREATEST x WRT m. P" == "GreatestM m (%x. P)"
+
+lemma GreatestMI2:
+     "[| P x;
+	 !!y. P y ==> m y <= m x;
+         !!x. [| P x; \\<forall>y. P y --> m y \\<le> m x |] ==> Q x |]
+      ==> Q (GreatestM m P)";
+apply (unfold GreatestM_def)
+apply (rule someI2_ex)
+apply  blast
+apply blast
+done
+
+lemma GreatestM_equality:
+ "[| P k;  !!x. P x ==> m x <= m k |]
+  ==> m (GREATEST x WRT m. P x) = (m k::'a::order)";
+apply (rule_tac m=m in GreatestMI2)
+apply   assumption
+apply  blast
+apply (blast intro!: order_antisym) 
+done
+
+lemma Greatest_equality:
+  "[| P (k::'a::order); !!x. P x ==> x <= k |] ==> (GREATEST x. P x) = k";
+apply (unfold Greatest_def)
+apply (erule GreatestM_equality)
+apply blast
+done
+
+lemma ex_has_greatest_nat_lemma:
+     "[|P k;  ALL x. P x --> (EX y. P y & ~ ((m y::nat) <= m x))|]  
+      ==> EX y. P y & ~ (m y < m k + n)"
+apply (induct_tac "n")
+apply force
+(*ind step*)
+apply (force simp add: le_Suc_eq)
+done
+
+lemma ex_has_greatest_nat: "[|P k;  ! y. P y --> m y < b|]  
+      ==> ? x. P x & (! y. P y --> (m y::nat) <= m x)"
+apply (rule ccontr)
+apply (cut_tac P = "P" and n = "b - m k" in ex_has_greatest_nat_lemma)
+apply (subgoal_tac [3] "m k <= b")
+apply auto
+done
+
+lemma GreatestM_nat_lemma: 
+     "[|P k;  ! y. P y --> m y < b|]  
+      ==> P (GreatestM m P) & (!y. P y --> (m y::nat) <= m (GreatestM m P))"
+apply (unfold GreatestM_def)
+apply (rule someI_ex)
+apply (erule ex_has_greatest_nat)
+apply assumption
+done
+
+lemmas GreatestM_natI = GreatestM_nat_lemma [THEN conjunct1, standard]
+
+lemma GreatestM_nat_le: "[|P x;  ! y. P y --> m y < b|]  
+      ==> (m x::nat) <= m (GreatestM m P)"
+apply (blast dest: GreatestM_nat_lemma [THEN conjunct2, THEN spec]) 
+done
+
+(** Specialization to GREATEST **)
+
+lemma GreatestI: 
+     "[|P (k::nat);  ! y. P y --> y < b|] ==> P (GREATEST x. P x)"
+
+apply (unfold Greatest_def)
+apply (rule GreatestM_natI)
+apply auto
+done
+
+lemma Greatest_le: 
+     "[|P x;  ! y. P y --> y < b|] ==> (x::nat) <= (GREATEST x. P x)"
+apply (unfold Greatest_def)
+apply (rule GreatestM_nat_le)
+apply auto
+done
+
+
+ML {*
+val LeastMI2 = thm "LeastMI2";
+val LeastM_equality = thm "LeastM_equality";
+val GreatestM_def = thm "GreatestM_def";
+val GreatestMI2 = thm "GreatestMI2";
+val GreatestM_equality = thm "GreatestM_equality";
+val Greatest_def = thm "Greatest_def";
+val Greatest_equality = thm "Greatest_equality";
+val GreatestM_natI = thm "GreatestM_natI";
+val GreatestM_nat_le = thm "GreatestM_nat_le";
+val GreatestI = thm "GreatestI";
+val Greatest_le = thm "Greatest_le";
+*}
+
+use "meson_lemmas.ML"
+use "Tools/meson.ML"
+setup meson_setup
+
+end

--- a/src/HOL/Integ/Int.thy	Tue Jul 24 11:25:54 2001 +0200
+++ b/src/HOL/Integ/Int.thy	Wed Jul 25 13:13:01 2001 +0200
@@ -6,7 +6,7 @@
 Type "int" is a linear order
 *)
 
-Int = IntDef +
+Int = IntDef + 
 
 instance int :: order (zle_refl,zle_trans,zle_anti_sym,int_less_le)
 instance int :: plus_ac0 (zadd_commute,zadd_assoc,zadd_zero)
@@ -14,7 +14,7 @@
 
 constdefs
   nat  :: int => nat
-  "nat(Z) == if neg Z then 0 else (@ m. Z = int m)"
+  "nat(Z) == if neg Z then 0 else (THE m. Z = int m)"
 
 defs
   zabs_def  "abs(i::int) == if i < 0 then -i else i"

--- a/src/HOL/Integ/IntDef.thy	Tue Jul 24 11:25:54 2001 +0200
+++ b/src/HOL/Integ/IntDef.thy	Wed Jul 25 13:13:01 2001 +0200
@@ -6,7 +6,7 @@
 The integers as equivalence classes over nat*nat.
 *)
 
-IntDef = Equiv + NatArith +
+IntDef = Equiv + NatArith + 
 constdefs
   intrel      :: "((nat * nat) * (nat * nat)) set"
   "intrel == {p. EX x1 y1 x2 y2. p=((x1::nat,y1),(x2,y2)) & x1+y2 = x2+y1}"

--- a/src/HOL/IsaMakefile	Tue Jul 24 11:25:54 2001 +0200
+++ b/src/HOL/IsaMakefile	Wed Jul 25 13:13:01 2001 +0200
@@ -78,7 +78,8 @@
   $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML $(SRC)/TFL/thry.ML \
   $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML Calculation.thy \
   Datatype.thy Datatype_Universe.ML Datatype_Universe.thy Divides.ML \
-  Divides.thy Finite.ML Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy HOL.ML \
+  Divides.thy Finite.ML Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy \
+  Hilbert_Choice.thy Hilbert_Choice_lemmas.ML HOL.ML \
   HOL.thy HOL_lemmas.ML Inductive.thy Integ/Bin.ML Integ/Bin.thy \
   Integ/Equiv.ML Integ/Equiv.thy Integ/Int.ML Integ/Int.thy \
   Integ/IntArith.ML Integ/IntArith.thy Integ/IntDef.ML Integ/IntDef.thy \

--- a/src/HOL/Nat.thy	Tue Jul 24 11:25:54 2001 +0200
+++ b/src/HOL/Nat.thy	Wed Jul 25 13:13:01 2001 +0200
@@ -6,7 +6,7 @@
 and * (for div, mod and dvd, see theory Divides).
 *)
 
-Nat = NatDef +
+Nat = NatDef + 
 
 (* type "nat" is a wellfounded linear order, and a datatype *)
 

--- a/src/HOL/NatArith.ML	Tue Jul 24 11:25:54 2001 +0200
+++ b/src/HOL/NatArith.ML	Wed Jul 25 13:13:01 2001 +0200
@@ -135,54 +135,5 @@
 
 
 
-(** GREATEST theorems for type "nat": not dual to LEAST, since there is
-    no greatest natural number.  [The LEAST proofs are in Nat.ML, but the
-    GREATEST proofs require more infrastructure.] **)
-
-Goal "[|P k;  ALL x. P x --> (EX y. P y & ~ ((m y::nat) <= m x))|] \
-\     ==> EX y. P y & ~ (m y < m k + n)";
-by (induct_tac "n" 1);
-by (Force_tac 1); 
-(*ind step*)
-by (force_tac (claset(), simpset() addsimps [le_Suc_eq]) 1); 
-qed "ex_has_greatest_nat_lemma";
-
-Goal "[|P k;  ! y. P y --> m y < b|] \
-\     ==> ? x. P x & (! y. P y --> (m y::nat) <= m x)";
-by (rtac ccontr 1); 
-by (cut_inst_tac [("P","P"),("n","b - m k")] ex_has_greatest_nat_lemma 1);
-by (subgoal_tac "m k <= b" 3);
-by Auto_tac;  
-qed "ex_has_greatest_nat";
-
-Goalw [GreatestM_def]
-     "[|P k;  ! y. P y --> m y < b|] \
-\     ==> P (GreatestM m P) & (!y. P y --> (m y::nat) <= m (GreatestM m P))";
-by (rtac someI_ex 1);
-by (etac ex_has_greatest_nat 1);
-by (assume_tac 1); 
-qed "GreatestM_nat_lemma";
-
-bind_thm ("GreatestM_natI", GreatestM_nat_lemma RS conjunct1);
-
-Goal "[|P x;  ! y. P y --> m y < b|] \
-\     ==> (m x::nat) <= m (GreatestM m P)";
-by (blast_tac (claset() addDs [GreatestM_nat_lemma RS conjunct2 RS spec]) 1);
-qed "GreatestM_nat_le";
-
-(** Specialization to GREATEST **)
-
-Goalw [Greatest_def]
-     "[|P (k::nat);  ! y. P y --> y < b|] ==> P (GREATEST x. P x)";
-by (rtac GreatestM_natI 1); 
-by Auto_tac;  
-qed "GreatestI";
-
-Goalw [Greatest_def]
-     "[|P x;  ! y. P y --> y < b|] ==> (x::nat) <= (GREATEST x. P x)";
-by (rtac GreatestM_nat_le 1); 
-by Auto_tac;  
-qed "Greatest_le";
-
 (*No analogue of not_less_Least or Least_Suc yet, since it isn't used much*)
 

--- a/src/HOL/Ord.thy	Tue Jul 24 11:25:54 2001 +0200
+++ b/src/HOL/Ord.thy	Wed Jul 25 13:13:01 2001 +0200
@@ -25,8 +25,8 @@
 local
 
 syntax (symbols)
-  "op <="       :: "['a::ord, 'a] => bool"             ("op \<le>")
-  "op <="       :: "['a::ord, 'a] => bool"             ("(_/ \<le> _)"  [50, 51] 50)
+  "op <="       :: "['a::ord, 'a] => bool"             ("op \\<le>")
+  "op <="       :: "['a::ord, 'a] => bool"             ("(_/ \\<le> _)"  [50, 51] 50)
 
 (*Tell Blast_tac about overloading of < and <= to reduce the risk of
   its applying a rule for the wrong type*)
@@ -76,57 +76,6 @@
 done
 
 
-(** Least value operator **)
-
-constdefs
-  LeastM   :: "['a => 'b::ord, 'a => bool] => 'a"
-              "LeastM m P == @x. P x & (!y. P y --> m x <= m y)"
-  Least    :: "('a::ord => bool) => 'a"               (binder "LEAST " 10)
-              "Least     == LeastM (%x. x)"
-
-syntax
- "@LeastM" :: "[pttrn, 'a=>'b::ord, bool] => 'a" ("LEAST _ WRT _. _" [0,4,10]10)
-translations
-                "LEAST x WRT m. P" == "LeastM m (%x. P)"
-
-lemma LeastMI2: "[| P x; !!y. P y ==> m x <= m y;
- !!x. [| P x; \<forall>y. P y --> m x \<le> m y |] ==> Q x
-		 |] ==> Q (LeastM m P)";
-apply (unfold LeastM_def)
-apply (rule someI2_ex)
-apply  blast
-apply blast
-done
-
-
-(** Greatest value operator **)
-
-constdefs
-  GreatestM   :: "['a => 'b::ord, 'a => bool] => 'a"
-              "GreatestM m P == @x. P x & (!y. P y --> m y <= m x)"
-  
-  Greatest    :: "('a::ord => bool) => 'a"         (binder "GREATEST " 10)
-              "Greatest     == GreatestM (%x. x)"
-
-syntax
- "@GreatestM" :: "[pttrn, 'a=>'b::ord, bool] => 'a"
-                                        ("GREATEST _ WRT _. _" [0,4,10]10)
-
-translations
-              "GREATEST x WRT m. P" == "GreatestM m (%x. P)"
-
-lemma GreatestMI2:
-     "[| P x;
-	 !!y. P y ==> m y <= m x;
-         !!x. [| P x; \<forall>y. P y --> m y \<le> m x |] ==> Q x |]
-      ==> Q (GreatestM m P)";
-apply (unfold GreatestM_def)
-apply (rule someI2_ex)
-apply  blast
-apply blast
-done
-
-
 section "Orders"
 
 axclass order < ord
@@ -216,36 +165,19 @@
 apply (blast intro: order_antisym)
 done
 
-lemma LeastM_equality:
- "[| P k; !!x. P x ==> m k <= m x |] ==> m (LEAST x WRT m. P x) = 
-     (m k::'a::order)";
-apply (rule LeastMI2)
-apply   assumption
-apply  blast
-apply (blast intro!: order_antisym) 
-done
+
+(** Least value operator **)
+
+(*We can no longer use LeastM because the latter requires Hilbert-AC*)
+constdefs
+  Least    :: "('a::ord => bool) => 'a"               (binder "LEAST " 10)
+    "Least P == THE x. P x & (ALL y. P y --> x <= y)"
 
 lemma Least_equality:
   "[| P (k::'a::order); !!x. P x ==> k <= x |] ==> (LEAST x. P x) = k";
-apply (unfold Least_def)
-apply (erule LeastM_equality)
-apply blast
-done
-
-lemma GreatestM_equality:
- "[| P k;  !!x. P x ==> m x <= m k |]
-  ==> m (GREATEST x WRT m. P x) = (m k::'a::order)";
-apply (rule_tac m=m in GreatestMI2)
-apply   assumption
-apply  blast
-apply (blast intro!: order_antisym) 
-done
-
-lemma Greatest_equality:
-  "[| P (k::'a::order); !!x. P x ==> x <= k |] ==> (GREATEST x. P x) = k";
-apply (unfold Greatest_def)
-apply (erule GreatestM_equality)
-apply blast
+apply (simp add: Least_def)
+apply (rule the_equality)
+apply (auto intro!: order_antisym) 
 done
 
 
@@ -381,10 +313,10 @@
   "_leEx"    :: "[idt, 'a, bool] => bool"  ("(3EX _<=_./ _)" [0, 0, 10] 10)
 
 syntax (symbols)
-  "_lessAll" :: "[idt, 'a, bool] => bool"  ("(3\<forall>_<_./ _)"  [0, 0, 10] 10)
-  "_lessEx"  :: "[idt, 'a, bool] => bool"  ("(3\<exists>_<_./ _)"  [0, 0, 10] 10)
-  "_leAll"   :: "[idt, 'a, bool] => bool"  ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10)
-  "_leEx"    :: "[idt, 'a, bool] => bool"  ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10)
+  "_lessAll" :: "[idt, 'a, bool] => bool"  ("(3\\<forall>_<_./ _)"  [0, 0, 10] 10)
+  "_lessEx"  :: "[idt, 'a, bool] => bool"  ("(3\\<exists>_<_./ _)"  [0, 0, 10] 10)
+  "_leAll"   :: "[idt, 'a, bool] => bool"  ("(3\\<forall>_\\<le>_./ _)" [0, 0, 10] 10)
+  "_leEx"    :: "[idt, 'a, bool] => bool"  ("(3\\<exists>_\\<le>_./ _)" [0, 0, 10] 10)
 
 syntax (HOL)
   "_lessAll" :: "[idt, 'a, bool] => bool"  ("(3! _<_./ _)"  [0, 0, 10] 10)
@@ -401,6 +333,8 @@
 
 ML
 {*
+val Least_def = thm "Least_def";
+val Least_equality = thm "Least_equality";
 val mono_def = thm "mono_def";
 val monoI = thm "monoI";
 val monoD = thm "monoD";
@@ -410,15 +344,6 @@
 val max_of_mono = thm "max_of_mono";
 val min_leastL = thm "min_leastL";
 val max_leastL = thm "max_leastL";
-val LeastMI2 = thm "LeastMI2";
-val LeastM_equality = thm "LeastM_equality";
-val Least_def = thm "Least_def";
-val Least_equality = thm "Least_equality";
-val GreatestM_def = thm "GreatestM_def";
-val GreatestMI2 = thm "GreatestMI2";
-val GreatestM_equality = thm "GreatestM_equality";
-val Greatest_def = thm "Greatest_def";
-val Greatest_equality = thm "Greatest_equality";
 val min_leastR = thm "min_leastR";
 val max_leastR = thm "max_leastR";
 val order_eq_refl = thm "order_eq_refl";

--- a/src/HOL/Product_Type.thy	Tue Jul 24 11:25:54 2001 +0200
+++ b/src/HOL/Product_Type.thy	Wed Jul 25 13:13:01 2001 +0200
@@ -30,9 +30,9 @@
 qed
 
 syntax (symbols)
-  "*"      :: "[type, type] => type"         ("(_ \<times>/ _)" [21, 20] 20)
+  "*"      :: "[type, type] => type"         ("(_ \\<times>/ _)" [21, 20] 20)
 syntax (HTML output)
-  "*"      :: "[type, type] => type"         ("(_ \<times>/ _)" [21, 20] 20)
+  "*"      :: "[type, type] => type"         ("(_ \\<times>/ _)" [21, 20] 20)
 
 
 (* abstract constants and syntax *)
@@ -74,8 +74,8 @@
   "A <*> B"      => "Sigma A (_K B)"
 
 syntax (symbols)
-  "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"  ("(3\<Sigma> _\<in>_./ _)"   10)
-  "@Times" :: "['a set,  'a => 'b set] => ('a * 'b) set"  ("_ \<times> _" [81, 80] 80)
+  "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"  ("(3\\<Sigma> _\\<in>_./ _)"   10)
+  "@Times" :: "['a set,  'a => 'b set] => ('a * 'b) set"  ("_ \\<times> _" [81, 80] 80)
 
 print_translation {* [("Sigma", dependent_tr' ("@Sigma", "@Times"))] *}
 
@@ -86,8 +86,8 @@
 
 defs
   Pair_def:     "Pair a b == Abs_Prod(Pair_Rep a b)"
-  fst_def:      "fst p == SOME a. EX b. p = (a, b)"
-  snd_def:      "snd p == SOME b. EX a. p = (a, b)"
+  fst_def:      "fst p == THE a. EX b. p = (a, b)"
+  snd_def:      "snd p == THE b. EX a. p = (a, b)"
   split_def:    "split == (%c p. c (fst p) (snd p))"
   prod_fun_def: "prod_fun f g == split(%x y.(f(x), g(y)))"
   Sigma_def:    "Sigma A B == UN x:A. UN y:B(x). {(x, y)}"

--- a/src/HOL/Product_Type_lemmas.ML	Tue Jul 24 11:25:54 2001 +0200
+++ b/src/HOL/Product_Type_lemmas.ML	Wed Jul 25 13:13:01 2001 +0200
@@ -192,13 +192,13 @@
 qed "split_Pair_apply";
 
 (*Can't be added to simpset: loops!*)
-Goal "(SOME x. P x) = (SOME (a,b). P(a,b))";
+Goal "(THE x. P x) = (THE (a,b). P(a,b))";
 by (simp_tac (simpset() addsimps [split_Pair_apply]) 1);
-qed "split_paired_Eps";
+qed "split_paired_The";
 
-Goalw [split_def] "Eps (split P) = (SOME xy. P (fst xy) (snd xy))";
+Goalw [split_def] "The (split P) = (THE xy. P (fst xy) (snd xy))";
 by (rtac refl 1);
-qed "Eps_split";
+qed "The_split";
 
 Goal "!!s t. (s=t) = (fst(s)=fst(t) & snd(s)=snd(t))";
 by (split_all_tac 1);
@@ -385,10 +385,10 @@
 qed "split_part";
 Addsimps [split_part];
 
-Goal "(@(x',y'). x = x' & y = y') = (x,y)";
+Goal "(THE (x',y'). x = x' & y = y') = (x,y)";
 by (Blast_tac 1);
-qed "Eps_split_eq";
-Addsimps [Eps_split_eq];
+qed "The_split_eq";
+Addsimps [The_split_eq];
 (*
 the following  would be slightly more general,
 but cannot be used as rewrite rule:
@@ -399,7 +399,7 @@
 by ( Simp_tac 1);
 by (split_all_tac 1);
 by (Asm_full_simp_tac 1);
-qed "Eps_split_eq";
+qed "The_split_eq";
 *)
 
 Goal "!!x y. [|fst x = fst y; snd x = snd y|] ==> x = y";

--- a/src/HOL/Relation.ML	Tue Jul 24 11:25:54 2001 +0200
+++ b/src/HOL/Relation.ML	Wed Jul 25 13:13:01 2001 +0200
@@ -333,7 +333,7 @@
 
 overload_1st_set "Relation.Image";
 
-Goalw [Image_def] "b : r``A = (? x:A. (x,b):r)";
+Goalw [Image_def] "b : r``A = (EX x:A. (x,b):r)";
 by (Blast_tac 1);
 qed "Image_iff";
 
@@ -422,7 +422,7 @@
 section "single_valued";
 
 Goalw [single_valued_def]
-     "!x y. (x,y):r --> (!z. (x,z):r --> y=z) ==> single_valued r";
+     "ALL x y. (x,y):r --> (ALL z. (x,z):r --> y=z) ==> single_valued r";
 by (assume_tac 1);
 qed "single_valuedI";
 
@@ -454,26 +454,18 @@
 by (Fast_tac 1);
 qed "fun_rel_comp_mono";
 
-Goalw [fun_rel_comp_def] "! x. ?! y. (f x, y) : R ==> ?! g. g : fun_rel_comp f R";
-by (res_inst_tac [("a","%x. @y. (f x, y) : R")] ex1I 1);
-by (rtac CollectI 1);
-by (rtac allI 1);
-by (etac allE 1);
-by (rtac (some_eq_ex RS iffD2) 1);
-by (etac ex1_implies_ex 1);
-by (rtac ext 1);
-by (etac CollectE 1);
-by (REPEAT (etac allE 1));
-by (rtac (some1_equality RS sym) 1);
-by (atac 1);
-by (atac 1);
+Goalw [fun_rel_comp_def]
+     "ALL x. EX! y. (f x, y) : R ==> EX! g. g : fun_rel_comp f R";
+by (res_inst_tac [("a","%x. THE y. (f x, y) : R")] ex1I 1);
+by (fast_tac (claset() addSDs [theI']) 1); 
+by (fast_tac (claset() addIs [ext, the1_equality RS sym]) 1);
 qed "fun_rel_comp_unique";
 
 
 section "inverse image";
 
 Goalw [trans_def,inv_image_def]
-    "!!r. trans r ==> trans (inv_image r f)";
+    "trans r ==> trans (inv_image r f)";
 by (Simp_tac 1);
 by (Blast_tac 1);
 qed "trans_inv_image";

--- a/src/HOL/Wellfounded_Recursion.ML	Tue Jul 24 11:25:54 2001 +0200
+++ b/src/HOL/Wellfounded_Recursion.ML	Wed Jul 25 13:13:01 2001 +0200
@@ -253,20 +253,15 @@
 (*** John Harrison, "Inductive definitions: automation and application" ***)
 
 Goalw [adm_wf_def]
-  "[| wf R; adm_wf R F |] ==> EX! y. (x, y) : wfrec_rel R F";
+  "[| adm_wf R F; wf R |] ==> EX! y. (x, y) : wfrec_rel R F";
 by (wf_ind_tac "x" [] 1);
 by (rtac ex1I 1);
-by (res_inst_tac [("g","%x. @y. (x, y) : wfrec_rel R F")] wfrec_rel.wfrecI 1);
-by (strip_tac 1);
-byev [etac allE 1, etac impE 1, atac 1];
-by (rtac (some_eq_ex RS ssubst) 1);
-by (etac ex1_implies_ex 1);
+by (res_inst_tac [("g","%x. THE y. (x, y) : wfrec_rel R F")] wfrec_rel.wfrecI 1);
+by (fast_tac (claset() addSDs [theI']) 1); 
 by (etac wfrec_rel.elim 1);
 by (Asm_full_simp_tac 1);
 byev [etac allE 1, etac allE 1, etac allE 1, etac mp 1];
-by (strip_tac 1);
-by (rtac (some_equality RS ssubst) 1);
-by (ALLGOALS Blast_tac);
+by (fast_tac (claset() addIs [the_equality RS sym]) 1);
 qed "wfrec_unique";
 
 Goalw [adm_wf_def] "adm_wf R (%f x. F (cut f R x) x)";
@@ -278,15 +273,14 @@
 
 Goalw [wfrec_def]
     "wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a";
-by (rtac (adm_lemma RSN (2, wfrec_unique) RS some1_equality) 1);
+by (rtac (adm_lemma RS wfrec_unique RS the1_equality) 1);
 by (atac 1);
 by (rtac wfrec_rel.wfrecI 1);
 by (strip_tac 1);
-by (rtac (some_eq_ex RS iffD2) 1);
-by (rtac (adm_lemma RSN (2, wfrec_unique) RS ex1_implies_ex) 1);
-by (atac 1);
+by (etac (adm_lemma RS wfrec_unique RS theI') 1);
 qed "wfrec";
 
+
 (*---------------------------------------------------------------------------
  * This form avoids giant explosions in proofs.  NOTE USE OF == 
  *---------------------------------------------------------------------------*)

--- a/src/HOL/Wellfounded_Recursion.thy	Tue Jul 24 11:25:54 2001 +0200
+++ b/src/HOL/Wellfounded_Recursion.thy	Wed Jul 25 13:13:01 2001 +0200
@@ -6,7 +6,7 @@
 Well-founded Recursion
 *)
 
-Wellfounded_Recursion = Transitive_Closure +
+Wellfounded_Recursion = Transitive_Closure + 
 
 consts
   wfrec_rel :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => ('a * 'b) set"
@@ -31,7 +31,7 @@
      (ALL z. (z, x) : R --> f z = g z) --> F f x = F g x"
 
   wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b"
-  "wfrec R F == %x. @y. (x, y) : wfrec_rel R (%f x. F (cut f R x) x)"
+  "wfrec R F == %x. THE y. (x, y) : wfrec_rel R (%f x. F (cut f R x) x)"
 
 axclass
   wellorder < linorder

--- a/src/HOL/Wellfounded_Relations.thy	Tue Jul 24 11:25:54 2001 +0200
+++ b/src/HOL/Wellfounded_Relations.thy	Wed Jul 25 13:13:01 2001 +0200
@@ -10,9 +10,9 @@
 separately.
 *)
 
-Wellfounded_Relations = Finite +
+Wellfounded_Relations = Finite + Hilbert_Choice + 
 
-(* actually belongs to theory Finite *)
+(* logically belongs in Finite.thy, but the theorems are proved in Finite.ML *)
 instance unit :: finite                  (finite_unit)
 instance "*" :: (finite,finite) finite   (finite_Prod)
 

--- a/src/HOL/cladata.ML	Tue Jul 24 11:25:54 2001 +0200
+++ b/src/HOL/cladata.ML	Wed Jul 25 13:13:01 2001 +0200
@@ -66,7 +66,7 @@
                        addSEs [conjE,disjE,impCE,FalseE,iffCE];
 
 (*Quantifier rules*)
-val HOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI, some_equality, the_equality] 
+val HOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI, the_equality] 
                      addSEs [exE] addEs [allE];
 
 val clasetup = [fn thy => (claset_ref_of thy := HOL_cs; thy)];

--- a/src/HOL/ex/Tarski.ML	Tue Jul 24 11:25:54 2001 +0200
+++ b/src/HOL/ex/Tarski.ML	Wed Jul 25 13:13:01 2001 +0200
@@ -84,12 +84,14 @@
                        (thm "cl_co");
 Addsimps [simp_CL, thm "cl_co"];
 
-Goalw [Ex_def] "(EX L. islub S cl L) = islub S cl (lub S cl)";
-by (simp_tac (simpset() addsimps [lub_def, least_def, islub_def]) 1);
+Goal "(EX L. islub S cl L) = islub S cl (lub S cl)";
+by (simp_tac (simpset() addsimps [lub_def, least_def, islub_def, 
+                                  some_eq_ex RS sym]) 1);
 qed "islub_lub";
 
-Goalw [Ex_def] "(EX G. isglb S cl G) = isglb S cl (glb S cl)";
-by (simp_tac (simpset() addsimps [glb_def, greatest_def, isglb_def]) 1);
+Goal "(EX G. isglb S cl G) = isglb S cl (glb S cl)";
+by (simp_tac (simpset() addsimps [glb_def, greatest_def, isglb_def, 
+                                  some_eq_ex RS sym]) 1);
 qed "isglb_glb";
 
 Goal "isglb S cl = islub S (dual cl)";

--- a/src/HOL/ex/mesontest.ML	Tue Jul 24 11:25:54 2001 +0200
+++ b/src/HOL/ex/mesontest.ML	Wed Jul 25 13:13:01 2001 +0200
@@ -33,7 +33,7 @@
 
 writeln"File HOL/ex/meson-test.";
 
-context Fun.thy;
+context Main.thy;
 
 (*Deep unifications can be required, esp. during transformation to clauses*)
 val orig_trace_bound = !Unify.trace_bound

--- a/src/HOL/ex/mesontest2.ML	Tue Jul 24 11:25:54 2001 +0200
+++ b/src/HOL/ex/mesontest2.ML	Wed Jul 25 13:13:01 2001 +0200
@@ -6,6 +6,9 @@
 MORE and MUCH HARDER test data for the MESON proof procedure
 
 Courtesy John Harrison 
+
+WARNING: there are many potential conflicts between variables used below
+and constants declared in HOL!
 *)
 
 (*All but the fastest are ignored to reduce build time*)
@@ -17,6 +20,8 @@
 
 set timing;
 
+context Main.thy;
+
 (* ========================================================================= *)
 (* 100 problems selected from the TPTP library                               *)
 (* ========================================================================= *)
@@ -155,10 +160,10 @@
 \  (! Y Z V1 V2 X V3 V4. sum(X::'a,Y,V1) & sum(X::'a,Z,V2) & product(Y::'a,Z,V3) & product(V1::'a,V2,V4) --> sum(X::'a,V3,V4)) &    \
 \  (! Y Z V3 X V1 V2 V4. sum(Y::'a,X,V1) & sum(Z::'a,X,V2) & product(Y::'a,Z,V3) & sum(V3::'a,X,V4) --> product(V1::'a,V2,V4)) &    \
 \  (! Y Z V1 V2 V3 X V4. sum(Y::'a,X,V1) & sum(Z::'a,X,V2) & product(Y::'a,Z,V3) & product(V1::'a,V2,V4) --> sum(V3::'a,X,V4)) &    \
-\  (! X. sum(inverse(X),X,multiplicative_identity)) &   \
-\  (! X. sum(X::'a,inverse(X),multiplicative_identity)) &   \
-\  (! X. product(inverse(X),X,additive_identity)) &     \
-\  (! X. product(X::'a,inverse(X),additive_identity)) &     \
+\  (! X. sum(INVERSE(X),X,multiplicative_identity)) &   \
+\  (! X. sum(X::'a,INVERSE(X),multiplicative_identity)) &   \
+\  (! X. product(INVERSE(X),X,additive_identity)) &     \
+\  (! X. product(X::'a,INVERSE(X),additive_identity)) &     \
 \  (! X Y U V. sum(X::'a,Y,U) & sum(X::'a,Y,V) --> equal(U::'a,V)) &        \
 \  (! X Y U V. product(X::'a,Y,U) & product(X::'a,Y,V) --> equal(U::'a,V)) &        \
 \  (! X Y W Z. equal(X::'a,Y) & sum(X::'a,W,Z) --> sum(Y::'a,W,Z)) &        \
@@ -171,7 +176,7 @@
 \  (! X W Y. equal(X::'a,Y) --> equal(add(W::'a,X),add(W::'a,Y))) & \
 \  (! X Y W. equal(X::'a,Y) --> equal(multiply(X::'a,W),multiply(Y::'a,W))) &       \
 \  (! X W Y. equal(X::'a,Y) --> equal(multiply(W::'a,X),multiply(W::'a,Y))) &       \
-\  (! X Y. equal(X::'a,Y) --> equal(inverse(X),inverse(Y))) &       \
+\  (! X Y. equal(X::'a,Y) --> equal(INVERSE(X),INVERSE(Y))) &       \
 \  (~product(x::'a,x,x)) --> False",
   meson_tac 1);
 
@@ -198,10 +203,10 @@
 \  (! Y Z V1 V2 X V3 V4. sum(X::'a,Y,V1) & sum(X::'a,Z,V2) & product(Y::'a,Z,V3) & product(V1::'a,V2,V4) --> sum(X::'a,V3,V4)) &    \
 \  (! Y Z V3 X V1 V2 V4. sum(Y::'a,X,V1) & sum(Z::'a,X,V2) & product(Y::'a,Z,V3) & sum(V3::'a,X,V4) --> product(V1::'a,V2,V4)) &    \
 \  (! Y Z V1 V2 V3 X V4. sum(Y::'a,X,V1) & sum(Z::'a,X,V2) & product(Y::'a,Z,V3) & product(V1::'a,V2,V4) --> sum(V3::'a,X,V4)) &    \
-\  (! X. sum(inverse(X),X,multiplicative_identity)) &   \
-\  (! X. sum(X::'a,inverse(X),multiplicative_identity)) &   \
-\  (! X. product(inverse(X),X,additive_identity)) &     \
-\  (! X. product(X::'a,inverse(X),additive_identity)) &     \
+\  (! X. sum(INVERSE(X),X,multiplicative_identity)) &   \
+\  (! X. sum(X::'a,INVERSE(X),multiplicative_identity)) &   \
+\  (! X. product(INVERSE(X),X,additive_identity)) &     \
+\  (! X. product(X::'a,INVERSE(X),additive_identity)) &     \
 \  (! X Y U V. sum(X::'a,Y,U) & sum(X::'a,Y,V) --> equal(U::'a,V)) &        \
 \  (! X Y U V. product(X::'a,Y,U) & product(X::'a,Y,V) --> equal(U::'a,V)) &        \
 \  (! X Y W Z. equal(X::'a,Y) & sum(X::'a,W,Z) --> sum(Y::'a,W,Z)) &        \
@@ -214,7 +219,7 @@
 \  (! X W Y. equal(X::'a,Y) --> equal(add(W::'a,X),add(W::'a,Y))) & \
 \  (! X Y W. equal(X::'a,Y) --> equal(multiply(X::'a,W),multiply(Y::'a,W))) &       \
 \  (! X W Y. equal(X::'a,Y) --> equal(multiply(W::'a,X),multiply(W::'a,Y))) &       \
-\  (! X Y. equal(X::'a,Y) --> equal(inverse(X),inverse(Y))) &       \
+\  (! X Y. equal(X::'a,Y) --> equal(INVERSE(X),INVERSE(Y))) &       \
 \  (~sum(x::'a,x,x)) --> False",
   meson_tac 1);
 
@@ -239,10 +244,10 @@
 \  (! Y Z V1 V2 X V3 V4. sum(X::'a,Y,V1) & sum(X::'a,Z,V2) & product(Y::'a,Z,V3) & product(V1::'a,V2,V4) --> sum(X::'a,V3,V4)) &    \
 \  (! Y Z V3 X V1 V2 V4. sum(Y::'a,X,V1) & sum(Z::'a,X,V2) & product(Y::'a,Z,V3) & sum(V3::'a,X,V4) --> product(V1::'a,V2,V4)) &    \
 \  (! Y Z V1 V2 V3 X V4. sum(Y::'a,X,V1) & sum(Z::'a,X,V2) & product(Y::'a,Z,V3) & product(V1::'a,V2,V4) --> sum(V3::'a,X,V4)) &    \
-\  (! X. sum(inverse(X),X,multiplicative_identity)) &   \
-\  (! X. sum(X::'a,inverse(X),multiplicative_identity)) &   \
-\  (! X. product(inverse(X),X,additive_identity)) &     \
-\  (! X. product(X::'a,inverse(X),additive_identity)) &     \
+\  (! X. sum(INVERSE(X),X,multiplicative_identity)) &   \
+\  (! X. sum(X::'a,INVERSE(X),multiplicative_identity)) &   \
+\  (! X. product(INVERSE(X),X,additive_identity)) &     \
+\  (! X. product(X::'a,INVERSE(X),additive_identity)) &     \
 \  (! X Y U V. sum(X::'a,Y,U) & sum(X::'a,Y,V) --> equal(U::'a,V)) &        \
 \  (! X Y U V. product(X::'a,Y,U) & product(X::'a,Y,V) --> equal(U::'a,V)) &        \
 \  (! X Y W Z. equal(X::'a,Y) & sum(X::'a,W,Z) --> sum(Y::'a,W,Z)) &        \
@@ -255,7 +260,7 @@
 \  (! X W Y. equal(X::'a,Y) --> equal(add(W::'a,X),add(W::'a,Y))) & \
 \  (! X Y W. equal(X::'a,Y) --> equal(multiply(X::'a,W),multiply(Y::'a,W))) &       \
 \  (! X W Y. equal(X::'a,Y) --> equal(multiply(W::'a,X),multiply(W::'a,Y))) &       \
-\  (! X Y. equal(X::'a,Y) --> equal(inverse(X),inverse(Y))) &       \
+\  (! X Y. equal(X::'a,Y) --> equal(INVERSE(X),INVERSE(Y))) &       \
 \  (~sum(x::'a,multiplicative_identity,multiplicative_identity)) --> False",
   meson_tac 1);
 
@@ -280,10 +285,10 @@
 \  (! Y Z V1 V2 X V3 V4. sum(X::'a,Y,V1) & sum(X::'a,Z,V2) & product(Y::'a,Z,V3) & product(V1::'a,V2,V4) --> sum(X::'a,V3,V4)) &    \
 \  (! Y Z V3 X V1 V2 V4. sum(Y::'a,X,V1) & sum(Z::'a,X,V2) & product(Y::'a,Z,V3) & sum(V3::'a,X,V4) --> product(V1::'a,V2,V4)) &    \
 \  (! Y Z V1 V2 V3 X V4. sum(Y::'a,X,V1) & sum(Z::'a,X,V2) & product(Y::'a,Z,V3) & product(V1::'a,V2,V4) --> sum(V3::'a,X,V4)) &    \
-\  (! X. sum(inverse(X),X,multiplicative_identity)) &   \
-\  (! X. sum(X::'a,inverse(X),multiplicative_identity)) &   \
-\  (! X. product(inverse(X),X,additive_identity)) &     \
-\  (! X. product(X::'a,inverse(X),additive_identity)) &     \
+\  (! X. sum(INVERSE(X),X,multiplicative_identity)) &   \
+\  (! X. sum(X::'a,INVERSE(X),multiplicative_identity)) &   \
+\  (! X. product(INVERSE(X),X,additive_identity)) &     \
+\  (! X. product(X::'a,INVERSE(X),additive_identity)) &     \
 \  (! X Y U V. sum(X::'a,Y,U) & sum(X::'a,Y,V) --> equal(U::'a,V)) &        \
 \  (! X Y U V. product(X::'a,Y,U) & product(X::'a,Y,V) --> equal(U::'a,V)) &        \
 \  (! X Y W Z. equal(X::'a,Y) & sum(X::'a,W,Z) --> sum(Y::'a,W,Z)) &        \
@@ -296,7 +301,7 @@
 \  (! X W Y. equal(X::'a,Y) --> equal(add(W::'a,X),add(W::'a,Y))) & \
 \  (! X Y W. equal(X::'a,Y) --> equal(multiply(X::'a,W),multiply(Y::'a,W))) &       \
 \  (! X W Y. equal(X::'a,Y) --> equal(multiply(W::'a,X),multiply(W::'a,Y))) &       \
-\  (! X Y. equal(X::'a,Y) --> equal(inverse(X),inverse(Y))) &       \
+\  (! X Y. equal(X::'a,Y) --> equal(INVERSE(X),INVERSE(Y))) &       \
 \  (~product(x::'a,additive_identity,additive_identity)) --> False",
   meson_tac 1);
 
@@ -321,10 +326,10 @@
 \  (! Y Z V1 V2 X V3 V4. sum(X::'a,Y,V1) & sum(X::'a,Z,V2) & product(Y::'a,Z,V3) & product(V1::'a,V2,V4) --> sum(X::'a,V3,V4)) &    \
 \  (! Y Z V3 X V1 V2 V4. sum(Y::'a,X,V1) & sum(Z::'a,X,V2) & product(Y::'a,Z,V3) & sum(V3::'a,X,V4) --> product(V1::'a,V2,V4)) &    \
 \  (! Y Z V1 V2 V3 X V4. sum(Y::'a,X,V1) & sum(Z::'a,X,V2) & product(Y::'a,Z,V3) & product(V1::'a,V2,V4) --> sum(V3::'a,X,V4)) &    \
-\  (! X. sum(inverse(X),X,multiplicative_identity)) &   \
-\  (! X. sum(X::'a,inverse(X),multiplicative_identity)) &   \
-\  (! X. product(inverse(X),X,additive_identity)) &     \
-\  (! X. product(X::'a,inverse(X),additive_identity)) &     \
+\  (! X. sum(INVERSE(X),X,multiplicative_identity)) &   \
+\  (! X. sum(X::'a,INVERSE(X),multiplicative_identity)) &   \
+\  (! X. product(INVERSE(X),X,additive_identity)) &     \
+\  (! X. product(X::'a,INVERSE(X),additive_identity)) &     \
 \  (! X Y U V. sum(X::'a,Y,U) & sum(X::'a,Y,V) --> equal(U::'a,V)) &        \
 \  (! X Y U V. product(X::'a,Y,U) & product(X::'a,Y,V) --> equal(U::'a,V)) &        \
 \  (! X Y W Z. equal(X::'a,Y) & sum(X::'a,W,Z) --> sum(Y::'a,W,Z)) &        \
@@ -337,8 +342,8 @@
 \  (! X W Y. equal(X::'a,Y) --> equal(add(W::'a,X),add(W::'a,Y))) & \
 \  (! X Y W. equal(X::'a,Y) --> equal(multiply(X::'a,W),multiply(Y::'a,W))) &       \
 \  (! X W Y. equal(X::'a,Y) --> equal(multiply(W::'a,X),multiply(W::'a,Y))) &       \
-\  (! X Y. equal(X::'a,Y) --> equal(inverse(X),inverse(Y))) &       \
-\  (~equal(inverse(additive_identity),multiplicative_identity)) --> False",
+\  (! X Y. equal(X::'a,Y) --> equal(INVERSE(X),INVERSE(Y))) &       \
+\  (~equal(INVERSE(additive_identity),multiplicative_identity)) --> False",
   meson_tac 1);
 
 (*4007 inferences so far.  Searching to depth 9.  13 secs*)
@@ -736,11 +741,11 @@
 \  (! E1 G1 F1. equal(E1::'a,F1) & failure_node(G1::'a,E1) --> failure_node(G1::'a,F1)) &   \
 \  (! H1 I1 J1. equal(H1::'a,I1) & siblings(H1::'a,J1) --> siblings(I1::'a,J1)) &   \
 \  (! K1 M1 L1. equal(K1::'a,L1) & siblings(M1::'a,K1) --> siblings(M1::'a,L1)) &   \
-\  (failure_node(n_left::'a,or(empty::'a,atom))) &      \
-\  (failure_node(n_right::'a,or(empty::'a,negate(atom)))) &     \
+\  (failure_node(n_left::'a,or(EMPTY::'a,atom))) &      \
+\  (failure_node(n_right::'a,or(EMPTY::'a,negate(atom)))) &     \
 \  (equal(n_left::'a,left_child_of(n))) &   \
 \  (equal(n_right::'a,right_child_of(n))) & \
-\  (! Z. ~failure_node(Z::'a,or(empty::'a,empty))) --> False",
+\  (! Z. ~failure_node(Z::'a,or(EMPTY::'a,EMPTY))) --> False",
   meson_tac 1);
 ****************)
 
@@ -1012,7 +1017,7 @@
 (*0 inferences so far.  Searching to depth 0.  0.2 secs*)
 val GEO079_1 = prove
  ("(! U V W X Y Z. right_angle(U::'a,V,W) & right_angle(X::'a,Y,Z) --> eq(U::'a,V,W,X,Y,Z)) &       \
-\  (! U V W X Y Z. congruent(U::'a,V,W,X,Y,Z) --> eq(U::'a,V,W,X,Y,Z)) &        \
+\  (! U V W X Y Z. CONGRUENT(U::'a,V,W,X,Y,Z) --> eq(U::'a,V,W,X,Y,Z)) &        \
 \  (! V W U X. trapezoid(U::'a,V,W,X) --> parallel(V::'a,W,U,X)) &      \
 \  (! U V X Y. parallel(U::'a,V,X,Y) --> eq(X::'a,V,U,V,X,Y)) & \
 \  (trapezoid(a::'a,b,c,d)) &       \
@@ -1027,13 +1032,13 @@
 \  (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) &  \
 \  (! X. product(identity::'a,X,X)) &       \
 \  (! X. product(X::'a,identity,X)) &       \
-\  (! X. product(inverse(X),X,identity)) &      \
-\  (! X. product(X::'a,inverse(X),identity)) &      \
+\  (! X. product(INVERSE(X),X,identity)) &      \
+\  (! X. product(X::'a,INVERSE(X),identity)) &      \
 \  (! X Y. product(X::'a,Y,multiply(X::'a,Y))) &        \
 \  (! X Y Z W. product(X::'a,Y,Z) & product(X::'a,Y,W) --> equal(Z::'a,W)) &        \
 \  (! Y U Z X V W. product(X::'a,Y,U) & product(Y::'a,Z,V) & product(U::'a,Z,W) --> product(X::'a,V,W)) &       \
 \  (! Y X V U Z W. product(X::'a,Y,U) & product(Y::'a,Z,V) & product(X::'a,V,W) --> product(U::'a,Z,W)) &       \
-\  (! X Y. equal(X::'a,Y) --> equal(inverse(X),inverse(Y))) &       \
+\  (! X Y. equal(X::'a,Y) --> equal(INVERSE(X),INVERSE(Y))) &       \
 \  (! X Y W. equal(X::'a,Y) --> equal(multiply(X::'a,W),multiply(Y::'a,W))) &       \
 \  (! X W Y. equal(X::'a,Y) --> equal(multiply(W::'a,X),multiply(W::'a,Y))) &       \
 \  (! X Y W Z. equal(X::'a,Y) & product(X::'a,W,Z) --> product(Y::'a,W,Z)) &        \
@@ -1052,13 +1057,13 @@
 \  (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) &  \
 \  (! X. product(identity::'a,X,X)) &       \
 \  (! X. product(X::'a,identity,X)) &       \
-\  (! X. product(inverse(X),X,identity)) &      \
-\  (! X. product(X::'a,inverse(X),identity)) &      \
+\  (! X. product(INVERSE(X),X,identity)) &      \
+\  (! X. product(X::'a,INVERSE(X),identity)) &      \
 \  (! X Y. product(X::'a,Y,multiply(X::'a,Y))) &        \
 \  (! X Y Z W. product(X::'a,Y,Z) & product(X::'a,Y,W) --> equal(Z::'a,W)) &        \
 \  (! Y U Z X V W. product(X::'a,Y,U) & product(Y::'a,Z,V) & product(U::'a,Z,W) --> product(X::'a,V,W)) &       \
 \  (! Y X V U Z W. product(X::'a,Y,U) & product(Y::'a,Z,V) & product(X::'a,V,W) --> product(U::'a,Z,W)) &       \
-\  (! X Y. equal(X::'a,Y) --> equal(inverse(X),inverse(Y))) &       \
+\  (! X Y. equal(X::'a,Y) --> equal(INVERSE(X),INVERSE(Y))) &       \
 \  (! X Y W. equal(X::'a,Y) --> equal(multiply(X::'a,W),multiply(Y::'a,W))) &       \
 \  (! X W Y. equal(X::'a,Y) --> equal(multiply(W::'a,X),multiply(W::'a,Y))) &       \
 \  (! X Y W Z. equal(X::'a,Y) & product(X::'a,W,Z) --> product(Y::'a,W,Z)) &        \
@@ -1080,13 +1085,13 @@
 \  (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) &  \
 \  (! X. product(identity::'a,X,X)) &       \
 \  (! X. product(X::'a,identity,X)) &       \
-\  (! X. product(inverse(X),X,identity)) &      \
-\  (! X. product(X::'a,inverse(X),identity)) &      \
+\  (! X. product(INVERSE(X),X,identity)) &      \
+\  (! X. product(X::'a,INVERSE(X),identity)) &      \
 \  (! X Y. product(X::'a,Y,multiply(X::'a,Y))) &        \
 \  (! X Y Z W. product(X::'a,Y,Z) & product(X::'a,Y,W) --> equal(Z::'a,W)) &        \
 \  (! Y U Z X V W. product(X::'a,Y,U) & product(Y::'a,Z,V) & product(U::'a,Z,W) --> product(X::'a,V,W)) &       \
 \  (! Y X V U Z W. product(X::'a,Y,U) & product(Y::'a,Z,V) & product(X::'a,V,W) --> product(U::'a,Z,W)) &       \
-\  (! X Y. equal(X::'a,Y) --> equal(inverse(X),inverse(Y))) &       \
+\  (! X Y. equal(X::'a,Y) --> equal(INVERSE(X),INVERSE(Y))) &       \
 \  (! X Y W. equal(X::'a,Y) --> equal(multiply(X::'a,W),multiply(Y::'a,W))) &       \
 \  (! X W Y. equal(X::'a,Y) --> equal(multiply(W::'a,X),multiply(W::'a,Y))) &       \
 \  (! X Y W Z. equal(X::'a,Y) & product(X::'a,W,Z) --> product(Y::'a,W,Z)) &        \
@@ -1094,8 +1099,8 @@
 \  (! X W Z Y. equal(X::'a,Y) & product(W::'a,Z,X) --> product(W::'a,Z,Y)) &        \
 \  (! A. product(A::'a,A,identity)) &       \
 \  (product(a::'a,b,c)) &   \
-\  (product(inverse(a),inverse(b),d)) & \
-\  (! A C B. product(inverse(A),inverse(B),C) --> product(A::'a,C,B)) &     \
+\  (product(INVERSE(a),INVERSE(b),d)) & \
+\  (! A C B. product(INVERSE(A),INVERSE(B),C) --> product(A::'a,C,B)) &     \
 \  (~product(c::'a,d,identity)) --> False",
   meson_tac 1);
 
@@ -1106,19 +1111,19 @@
 \  (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) &  \
 \  (! X. product(identity::'a,X,X)) &       \
 \  (! X. product(X::'a,identity,X)) &       \
-\  (! X. product(inverse(X),X,identity)) &      \
-\  (! X. product(X::'a,inverse(X),identity)) &      \
+\  (! X. product(INVERSE(X),X,identity)) &      \
+\  (! X. product(X::'a,INVERSE(X),identity)) &      \
 \  (! X Y. product(X::'a,Y,multiply(X::'a,Y))) &        \
 \  (! X Y Z W. product(X::'a,Y,Z) & product(X::'a,Y,W) --> equal(Z::'a,W)) &        \
 \  (! Y U Z X V W. product(X::'a,Y,U) & product(Y::'a,Z,V) & product(U::'a,Z,W) --> product(X::'a,V,W)) &       \
 \  (! Y X V U Z W. product(X::'a,Y,U) & product(Y::'a,Z,V) & product(X::'a,V,W) --> product(U::'a,Z,W)) &       \
-\  (! X Y. equal(X::'a,Y) --> equal(inverse(X),inverse(Y))) &       \
+\  (! X Y. equal(X::'a,Y) --> equal(INVERSE(X),INVERSE(Y))) &       \
 \  (! X Y W. equal(X::'a,Y) --> equal(multiply(X::'a,W),multiply(Y::'a,W))) &       \
 \  (! X W Y. equal(X::'a,Y) --> equal(multiply(W::'a,X),multiply(W::'a,Y))) &       \
 \  (! X Y W Z. equal(X::'a,Y) & product(X::'a,W,Z) --> product(Y::'a,W,Z)) &        \
 \  (! X W Y Z. equal(X::'a,Y) & product(W::'a,X,Z) --> product(W::'a,Y,Z)) &        \
 \  (! X W Z Y. equal(X::'a,Y) & product(W::'a,Z,X) --> product(W::'a,Z,Y)) &        \
-\  (! A B C. subgroup_member(A) & subgroup_member(B) & product(A::'a,inverse(B),C) --> subgroup_member(C)) &        \
+\  (! A B C. subgroup_member(A) & subgroup_member(B) & product(A::'a,INVERSE(B),C) --> subgroup_member(C)) &        \
 \  (! A B. equal(A::'a,B) & subgroup_member(A) --> subgroup_member(B)) &    \
 \  (! A. subgroup_member(A) --> product(another_identity::'a,A,A)) &        \
 \  (! A. subgroup_member(A) --> product(A::'a,another_identity,A)) &        \
@@ -1130,7 +1135,7 @@
 \  (! B C D A. product(A::'a,B,C) & product(D::'a,B,C) --> equal(D::'a,A)) &        \
 \  (subgroup_member(a)) &       \
 \  (subgroup_member(another_identity)) &        \
-\  (~equal(inverse(a),another_inverse(a))) --> False",
+\  (~equal(INVERSE(a),another_inverse(a))) --> False",
   meson_tac 1);
 
 (*163 inferences so far.  Searching to depth 11.  0.3 secs*)
@@ -1139,7 +1144,7 @@
 \  (! X Y Z W. product(X::'a,Y,Z) & product(X::'a,Y,W) --> equal(Z::'a,W)) &        \
 \  (! Y U Z X V W. product(X::'a,Y,U) & product(Y::'a,Z,V) & product(U::'a,Z,W) --> product(X::'a,V,W)) &       \
 \  (! Y X V U Z W. product(X::'a,Y,U) & product(Y::'a,Z,V) & product(X::'a,V,W) --> product(U::'a,Z,W)) &       \
-\  (! A. product(A::'a,inverse(A),identity)) &      \
+\  (! A. product(A::'a,INVERSE(A),identity)) &      \
 \  (! A. product(A::'a,identity,A)) &       \
 \  (! A. ~product(A::'a,a,identity)) --> False",
   meson_tac 1);
@@ -1149,18 +1154,18 @@
  ("(! X Y. product(X::'a,Y,multiply(X::'a,Y))) &        \
 \  (! X. product(identity::'a,X,X)) &       \
 \  (! X. product(X::'a,identity,X)) &       \
-\  (! X. product(X::'a,inverse(X),identity)) &      \
+\  (! X. product(X::'a,INVERSE(X),identity)) &      \
 \  (! Y U Z X V W. product(X::'a,Y,U) & product(Y::'a,Z,V) & product(U::'a,Z,W) --> product(X::'a,V,W)) &       \
 \  (! Y X V U Z W. product(X::'a,Y,U) & product(Y::'a,Z,V) & product(X::'a,V,W) --> product(U::'a,Z,W)) &       \
-\  (! B A C. subgroup_member(A) & subgroup_member(B) & product(B::'a,inverse(A),C) --> subgroup_member(C)) &        \
+\  (! B A C. subgroup_member(A) & subgroup_member(B) & product(B::'a,INVERSE(A),C) --> subgroup_member(C)) &        \
 \  (subgroup_member(a)) &       \
-\  (~subgroup_member(inverse(a))) --> False",
+\  (~subgroup_member(INVERSE(a))) --> False",
   meson_tac 1);
 
 (*3287 inferences so far.  Searching to depth 14.  3.5 secs*)
 val GRP047_2 = prove_hard
  ("(! X. product(identity::'a,X,X)) &       \
-\  (! X. product(inverse(X),X,identity)) &      \
+\  (! X. product(INVERSE(X),X,identity)) &      \
 \  (! X Y. product(X::'a,Y,multiply(X::'a,Y))) &        \
 \  (! X Y Z W. product(X::'a,Y,Z) & product(X::'a,Y,W) --> equal(Z::'a,W)) &        \
 \  (! Y U Z X V W. product(X::'a,Y,U) & product(Y::'a,Z,V) & product(U::'a,Z,W) --> product(X::'a,V,W)) &       \
@@ -1189,9 +1194,9 @@
 \  (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
 \  (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) &  \
 \  (! X. equal(multiply(identity::'a,X),X)) &       \
-\  (! X. equal(multiply(inverse(X),X),identity)) &      \
+\  (! X. equal(multiply(INVERSE(X),X),identity)) &      \
 \  (! X Y Z. equal(multiply(multiply(X::'a,Y),Z),multiply(X::'a,multiply(Y::'a,Z)))) &      \
-\  (! A B. equal(A::'a,B) --> equal(inverse(A),inverse(B))) &       \
+\  (! A B. equal(A::'a,B) --> equal(INVERSE(A),INVERSE(B))) &       \
 \  (! C D E. equal(C::'a,D) --> equal(multiply(C::'a,E),multiply(D::'a,E))) &       \
 \  (! F' H G. equal(F'::'a,G) --> equal(multiply(H::'a,F'),multiply(H::'a,G))) &    \
 \  (! Y X. equal(greatest_lower_bound(X::'a,Y),greatest_lower_bound(Y::'a,X))) &        \
@@ -1222,9 +1227,9 @@
 \  (! Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \
 \  (! Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z)) &  \
 \  (! X. equal(multiply(identity::'a,X),X)) &       \
-\  (! X. equal(multiply(inverse(X),X),identity)) &      \
+\  (! X. equal(multiply(INVERSE(X),X),identity)) &      \
 \  (! X Y Z. equal(multiply(multiply(X::'a,Y),Z),multiply(X::'a,multiply(Y::'a,Z)))) &      \
-\  (! A B. equal(A::'a,B) --> equal(inverse(A),inverse(B))) &       \
+\  (! A B. equal(A::'a,B) --> equal(INVERSE(A),INVERSE(B))) &       \
 \  (! C D E. equal(C::'a,D) --> equal(multiply(C::'a,E),multiply(D::'a,E))) &       \
 \  (! F' H G. equal(F'::'a,G) --> equal(multiply(H::'a,F'),multiply(H::'a,G))) &    \
 \  (! Y X. equal(greatest_lower_bound(X::'a,Y),greatest_lower_bound(Y::'a,X))) &        \
@@ -1246,7 +1251,7 @@
 \  (! A B C. equal(A::'a,B) --> equal(multiply(A::'a,C),multiply(B::'a,C))) &       \
 \  (! A C B. equal(A::'a,B) --> equal(multiply(C::'a,A),multiply(C::'a,B))) &       \
 \  (equal(least_upper_bound(a::'a,b),b)) &  \
-\  (~equal(least_upper_bound(multiply(inverse(c),multiply(a::'a,c)),multiply(inverse(c),multiply(b::'a,c))),multiply(inverse(c),multiply(b::'a,c)))) --> False",
+\  (~equal(least_upper_bound(multiply(INVERSE(c),multiply(a::'a,c)),multiply(INVERSE(c),multiply(b::'a,c))),multiply(INVERSE(c),multiply(b::'a,c)))) --> False",
   meson_tac 1);
 
 (*250258 inferences so far.  Searching to depth 16.  406.2 secs*)
@@ -1664,8 +1669,8 @@
 \  (! X. subclass(flip(X),cross_product(cross_product(universal_class::'a,universal_class),universal_class))) &     \
 \  (! V U W X. member(ordered_pair(ordered_pair(U::'a,V),W),flip(X)) --> member(ordered_pair(ordered_pair(V::'a,U),W),X)) &     \
 \  (! U V W X. member(ordered_pair(ordered_pair(V::'a,U),W),X) & member(ordered_pair(ordered_pair(U::'a,V),W),cross_product(cross_product(universal_class::'a,universal_class),universal_class)) --> member(ordered_pair(ordered_pair(U::'a,V),W),flip(X))) &   \
-\  (! Y. equal(domain_of(flip(cross_product(Y::'a,universal_class))),inverse(Y))) & \
-\  (! Z. equal(domain_of(inverse(Z)),range_of(Z))) &    \
+\  (! Y. equal(domain_of(flip(cross_product(Y::'a,universal_class))),INVERSE(Y))) & \
+\  (! Z. equal(domain_of(INVERSE(Z)),range_of(Z))) &    \
 \  (! Z X Y. equal(first(not_subclass_element(restrct(Z::'a,X,singleton(Y)),null_class)),domain(Z::'a,X,Y))) & \
 \  (! Z X Y. equal(second(not_subclass_element(restrct(Z::'a,singleton(X),Y),null_class)),rng(Z::'a,X,Y))) & \
 \  (! Xr X. equal(range_of(restrct(Xr::'a,X,universal_class)),image_(Xr::'a,X))) &      \
@@ -1686,11 +1691,11 @@
 \  (! Yr Xr. subclass(compos(Yr::'a,Xr),cross_product(universal_class::'a,universal_class))) & \
 \  (! Z Yr Xr Y. member(ordered_pair(Y::'a,Z),compos(Yr::'a,Xr)) --> member(Z::'a,image_(Yr::'a,image_(Xr::'a,singleton(Y))))) &     \
 \  (! Y Z Yr Xr. member(Z::'a,image_(Yr::'a,image_(Xr::'a,singleton(Y)))) & member(ordered_pair(Y::'a,Z),cross_product(universal_class::'a,universal_class)) --> member(ordered_pair(Y::'a,Z),compos(Yr::'a,Xr))) &  \
-\  (! X. single_valued_class(X) --> subclass(compos(X::'a,inverse(X)),identity_relation)) &        \
-\  (! X. subclass(compos(X::'a,inverse(X)),identity_relation) --> single_valued_class(X)) &        \
+\  (! X. single_valued_class(X) --> subclass(compos(X::'a,INVERSE(X)),identity_relation)) &        \
+\  (! X. subclass(compos(X::'a,INVERSE(X)),identity_relation) --> single_valued_class(X)) &        \
 \  (! Xf. function(Xf) --> subclass(Xf::'a,cross_product(universal_class::'a,universal_class))) &       \
-\  (! Xf. function(Xf) --> subclass(compos(Xf::'a,inverse(Xf)),identity_relation)) &       \
-\  (! Xf. subclass(Xf::'a,cross_product(universal_class::'a,universal_class)) & subclass(compos(Xf::'a,inverse(Xf)),identity_relation) --> function(Xf)) & \
+\  (! Xf. function(Xf) --> subclass(compos(Xf::'a,INVERSE(Xf)),identity_relation)) &       \
+\  (! Xf. subclass(Xf::'a,cross_product(universal_class::'a,universal_class)) & subclass(compos(Xf::'a,INVERSE(Xf)),identity_relation) --> function(Xf)) & \
 \  (! Xf X. function(Xf) & member(X::'a,universal_class) --> member(image_(Xf::'a,X),universal_class)) & \
 \  (! X. equal(X::'a,null_class) | member(regular(X),X)) & \
 \  (! X. equal(X::'a,null_class) | equal(intersection(X::'a,regular(X)),null_class)) & \
@@ -1698,12 +1703,12 @@
 \  (function(choice)) & \
 \  (! Y. member(Y::'a,universal_class) --> equal(Y::'a,null_class) | member(apply(choice::'a,Y),Y)) &      \
 \  (! Xf. one_to_one(Xf) --> function(Xf)) &    \
-\  (! Xf. one_to_one(Xf) --> function(inverse(Xf))) &   \
-\  (! Xf. function(inverse(Xf)) & function(Xf) --> one_to_one(Xf)) &    \
-\  (equal(intersection(cross_product(universal_class::'a,universal_class),intersection(cross_product(universal_class::'a,universal_class),complement(compos(complement(element_relation),inverse(element_relation))))),subset_relation)) &     \
-\  (equal(intersection(inverse(subset_relation),subset_relation),identity_relation)) &  \
+\  (! Xf. one_to_one(Xf) --> function(INVERSE(Xf))) &   \
+\  (! Xf. function(INVERSE(Xf)) & function(Xf) --> one_to_one(Xf)) &    \
+\  (equal(intersection(cross_product(universal_class::'a,universal_class),intersection(cross_product(universal_class::'a,universal_class),complement(compos(complement(element_relation),INVERSE(element_relation))))),subset_relation)) &     \
+\  (equal(intersection(INVERSE(subset_relation),subset_relation),identity_relation)) &  \
 \  (! Xr. equal(complement(domain_of(intersection(Xr::'a,identity_relation))),diagonalise(Xr))) &   \
-\  (! X. equal(intersection(domain_of(X),diagonalise(compos(inverse(element_relation),X))),cantor(X))) &       \
+\  (! X. equal(intersection(domain_of(X),diagonalise(compos(INVERSE(element_relation),X))),cantor(X))) &       \
 \  (! Xf. operation(Xf) --> function(Xf)) &     \
 \  (! Xf. operation(Xf) --> equal(cross_product(domain_of(domain_of(Xf)),domain_of(domain_of(Xf))),domain_of(Xf))) &    \
 \  (! Xf. operation(Xf) --> subclass(range_of(Xf),domain_of(domain_of(Xf)))) &  \
@@ -1739,7 +1744,7 @@
 \  (! C2 E2 D2. equal(C2::'a,D2) --> equal(image_(E2::'a,C2),image_(E2::'a,D2))) &    \
 \  (! F2 G2 H2. equal(F2::'a,G2) --> equal(intersection(F2::'a,H2),intersection(G2::'a,H2))) &      \
 \  (! I2 K2 J2. equal(I2::'a,J2) --> equal(intersection(K2::'a,I2),intersection(K2::'a,J2))) &      \
-\  (! L2 M2. equal(L2::'a,M2) --> equal(inverse(L2),inverse(M2))) & \
+\  (! L2 M2. equal(L2::'a,M2) --> equal(INVERSE(L2),INVERSE(M2))) & \
 \  (! N2 O2 P2 Q2. equal(N2::'a,O2) --> equal(not_homomorphism1(N2::'a,P2,Q2),not_homomorphism1(O2::'a,P2,Q2))) &   \
 \  (! R2 T2 S2 U2. equal(R2::'a,S2) --> equal(not_homomorphism1(T2::'a,R2,U2),not_homomorphism1(T2::'a,S2,U2))) &   \
 \  (! V2 X2 Y2 W2. equal(V2::'a,W2) --> equal(not_homomorphism1(X2::'a,Y2,V2),not_homomorphism1(X2::'a,Y2,W2))) &   \
@@ -1792,9 +1797,9 @@
 \  (subclass(domain_relation::'a,cross_product(universal_class::'a,universal_class))) & \
 \  (! X Y. member(ordered_pair(X::'a,Y),domain_relation) --> equal(domain_of(X),Y)) &       \
 \  (! X. member(X::'a,universal_class) --> member(ordered_pair(X::'a,domain_of(X)),domain_relation)) &  \
-\  (! X. equal(first(not_subclass_element(compos(X::'a,inverse(X)),identity_relation)),single_valued1(X))) &       \
-\  (! X. equal(second(not_subclass_element(compos(X::'a,inverse(X)),identity_relation)),single_valued2(X))) &      \
-\  (! X. equal(domain(X::'a,image_(inverse(X),singleton(single_valued1(X))),single_valued2(X)),single_valued3(X))) & \
+\  (! X. equal(first(not_subclass_element(compos(X::'a,INVERSE(X)),identity_relation)),single_valued1(X))) &       \
+\  (! X. equal(second(not_subclass_element(compos(X::'a,INVERSE(X)),identity_relation)),single_valued2(X))) &      \
+\  (! X. equal(domain(X::'a,image_(INVERSE(X),singleton(single_valued1(X))),single_valued2(X)),single_valued3(X))) & \
 \  (equal(intersection(complement(compos(element_relation::'a,complement(identity_relation))),element_relation),singleton_relation)) &     \
 \  (subclass(application_function::'a,cross_product(universal_class::'a,cross_product(universal_class::'a,universal_class)))) &     \
 \  (! Z Y X. member(ordered_pair(X::'a,ordered_pair(Y::'a,Z)),application_function) --> member(Y::'a,domain_of(X))) &       \
@@ -1811,15 +1816,15 @@
 \  (! X2 Y2 Z2 A3. equal(X2::'a,Y2) & maps(X2::'a,Z2,A3) --> maps(Y2::'a,Z2,A3)) &  \
 \  (! B3 D3 C3 E3. equal(B3::'a,C3) & maps(D3::'a,B3,E3) --> maps(D3::'a,C3,E3)) &  \
 \  (! F3 H3 I3 G3. equal(F3::'a,G3) & maps(H3::'a,I3,F3) --> maps(H3::'a,I3,G3)) &  \
-\  (! X. equal(union(X::'a,inverse(X)),symmetrization_of(X))) &     \
+\  (! X. equal(union(X::'a,INVERSE(X)),symmetrization_of(X))) &     \
 \  (! X Y. irreflexive(X::'a,Y) --> subclass(restrct(X::'a,Y,Y),complement(identity_relation))) &      \
 \  (! X Y. subclass(restrct(X::'a,Y,Y),complement(identity_relation)) --> irreflexive(X::'a,Y)) &      \
 \  (! Y X. connected(X::'a,Y) --> subclass(cross_product(Y::'a,Y),union(identity_relation::'a,symmetrization_of(X)))) &     \
 \  (! X Y. subclass(cross_product(Y::'a,Y),union(identity_relation::'a,symmetrization_of(X))) --> connected(X::'a,Y)) &     \
 \  (! Xr Y. transitive(Xr::'a,Y) --> subclass(compos(restrct(Xr::'a,Y,Y),restrct(Xr::'a,Y,Y)),restrct(Xr::'a,Y,Y))) &       \
 \  (! Xr Y. subclass(compos(restrct(Xr::'a,Y,Y),restrct(Xr::'a,Y,Y)),restrct(Xr::'a,Y,Y)) --> transitive(Xr::'a,Y)) &       \
-\  (! Xr Y. asymmetric(Xr::'a,Y) --> equal(restrct(intersection(Xr::'a,inverse(Xr)),Y,Y),null_class)) &        \
-\  (! Xr Y. equal(restrct(intersection(Xr::'a,inverse(Xr)),Y,Y),null_class) --> asymmetric(Xr::'a,Y)) &        \
+\  (! Xr Y. asymmetric(Xr::'a,Y) --> equal(restrct(intersection(Xr::'a,INVERSE(Xr)),Y,Y),null_class)) &        \
+\  (! Xr Y. equal(restrct(intersection(Xr::'a,INVERSE(Xr)),Y,Y),null_class) --> asymmetric(Xr::'a,Y)) &        \
 \  (! Xr Y Z. equal(segment(Xr::'a,Y,Z),domain_of(restrct(Xr::'a,Y,singleton(Z))))) &  \
 \  (! X Y. well_ordering(X::'a,Y) --> connected(X::'a,Y)) &     \
 \  (! Y Xr U. well_ordering(Xr::'a,Y) & subclass(U::'a,Y) --> equal(U::'a,null_class) | member(least(Xr::'a,U),U)) &   \
@@ -1934,8 +1939,8 @@
 \  (! X. subclass(flip(X),cross_product(cross_product(universal_class::'a,universal_class),universal_class))) &     \
 \  (! V U W X. member(ordered_pair(ordered_pair(U::'a,V),W),flip(X)) --> member(ordered_pair(ordered_pair(V::'a,U),W),X)) &     \
 \  (! U V W X. member(ordered_pair(ordered_pair(V::'a,U),W),X) & member(ordered_pair(ordered_pair(U::'a,V),W),cross_product(cross_product(universal_class::'a,universal_class),universal_class)) --> member(ordered_pair(ordered_pair(U::'a,V),W),flip(X))) &   \
-\  (! Y. equal(domain_of(flip(cross_product(Y::'a,universal_class))),inverse(Y))) & \
-\  (! Z. equal(domain_of(inverse(Z)),range_of(Z))) &    \
+\  (! Y. equal(domain_of(flip(cross_product(Y::'a,universal_class))),INVERSE(Y))) & \
+\  (! Z. equal(domain_of(INVERSE(Z)),range_of(Z))) &    \
 \  (! Z X Y. equal(first(not_subclass_element(restrct(Z::'a,X,singleton(Y)),null_class)),domain(Z::'a,X,Y))) & \
 \  (! Z X Y. equal(second(not_subclass_element(restrct(Z::'a,singleton(X),Y),null_class)),rng(Z::'a,X,Y))) & \
 \  (! Xr X. equal(range_of(restrct(Xr::'a,X,universal_class)),image_(Xr::'a,X))) &      \
@@ -1956,11 +1961,11 @@
 \  (! Yr Xr. subclass(compos(Yr::'a,Xr),cross_product(universal_class::'a,universal_class))) & \
 \  (! Z Yr Xr Y. member(ordered_pair(Y::'a,Z),compos(Yr::'a,Xr)) --> member(Z::'a,image_(Yr::'a,image_(Xr::'a,singleton(Y))))) &     \
 \  (! Y Z Yr Xr. member(Z::'a,image_(Yr::'a,image_(Xr::'a,singleton(Y)))) & member(ordered_pair(Y::'a,Z),cross_product(universal_class::'a,universal_class)) --> member(ordered_pair(Y::'a,Z),compos(Yr::'a,Xr))) &  \
-\  (! X. single_valued_class(X) --> subclass(compos(X::'a,inverse(X)),identity_relation)) &        \
-\  (! X. subclass(compos(X::'a,inverse(X)),identity_relation) --> single_valued_class(X)) &        \
+\  (! X. single_valued_class(X) --> subclass(compos(X::'a,INVERSE(X)),identity_relation)) &        \
+\  (! X. subclass(compos(X::'a,INVERSE(X)),identity_relation) --> single_valued_class(X)) &        \
 \  (! Xf. function(Xf) --> subclass(Xf::'a,cross_product(universal_class::'a,universal_class))) &       \
-\  (! Xf. function(Xf) --> subclass(compos(Xf::'a,inverse(Xf)),identity_relation)) &       \
-\  (! Xf. subclass(Xf::'a,cross_product(universal_class::'a,universal_class)) & subclass(compos(Xf::'a,inverse(Xf)),identity_relation) --> function(Xf)) & \
+\  (! Xf. function(Xf) --> subclass(compos(Xf::'a,INVERSE(Xf)),identity_relation)) &       \
+\  (! Xf. subclass(Xf::'a,cross_product(universal_class::'a,universal_class)) & subclass(compos(Xf::'a,INVERSE(Xf)),identity_relation) --> function(Xf)) & \
 \  (! Xf X. function(Xf) & member(X::'a,universal_class) --> member(image_(Xf::'a,X),universal_class)) & \
 \  (! X. equal(X::'a,null_class) | member(regular(X),X)) & \
 \  (! X. equal(X::'a,null_class) | equal(intersection(X::'a,regular(X)),null_class)) & \
@@ -1968,12 +1973,12 @@
 \  (function(choice)) & \
 \  (! Y. member(Y::'a,universal_class) --> equal(Y::'a,null_class) | member(apply(choice::'a,Y),Y)) &      \
 \  (! Xf. one_to_one(Xf) --> function(Xf)) &    \
-\  (! Xf. one_to_one(Xf) --> function(inverse(Xf))) &   \
-\  (! Xf. function(inverse(Xf)) & function(Xf) --> one_to_one(Xf)) &    \
-\  (equal(intersection(cross_product(universal_class::'a,universal_class),intersection(cross_product(universal_class::'a,universal_class),complement(compos(complement(element_relation),inverse(element_relation))))),subset_relation)) &     \
-\  (equal(intersection(inverse(subset_relation),subset_relation),identity_relation)) &  \
+\  (! Xf. one_to_one(Xf) --> function(INVERSE(Xf))) &   \
+\  (! Xf. function(INVERSE(Xf)) & function(Xf) --> one_to_one(Xf)) &    \
+\  (equal(intersection(cross_product(universal_class::'a,universal_class),intersection(cross_product(universal_class::'a,universal_class),complement(compos(complement(element_relation),INVERSE(element_relation))))),subset_relation)) &     \
+\  (equal(intersection(INVERSE(subset_relation),subset_relation),identity_relation)) &  \
 \  (! Xr. equal(complement(domain_of(intersection(Xr::'a,identity_relation))),diagonalise(Xr))) &   \
-\  (! X. equal(intersection(domain_of(X),diagonalise(compos(inverse(element_relation),X))),cantor(X))) &       \
+\  (! X. equal(intersection(domain_of(X),diagonalise(compos(INVERSE(element_relation),X))),cantor(X))) &       \
 \  (! Xf. operation(Xf) --> function(Xf)) &     \
 \  (! Xf. operation(Xf) --> equal(cross_product(domain_of(domain_of(Xf)),domain_of(domain_of(Xf))),domain_of(Xf))) &    \
 \  (! Xf. operation(Xf) --> subclass(range_of(Xf),domain_of(domain_of(Xf)))) &  \
@@ -2009,7 +2014,7 @@
 \  (! C2 E2 D2. equal(C2::'a,D2) --> equal(image_(E2::'a,C2),image_(E2::'a,D2))) &    \
 \  (! F2 G2 H2. equal(F2::'a,G2) --> equal(intersection(F2::'a,H2),intersection(G2::'a,H2))) &      \
 \  (! I2 K2 J2. equal(I2::'a,J2) --> equal(intersection(K2::'a,I2),intersection(K2::'a,J2))) &      \
-\  (! L2 M2. equal(L2::'a,M2) --> equal(inverse(L2),inverse(M2))) & \
+\  (! L2 M2. equal(L2::'a,M2) --> equal(INVERSE(L2),INVERSE(M2))) & \
 \  (! N2 O2 P2 Q2. equal(N2::'a,O2) --> equal(not_homomorphism1(N2::'a,P2,Q2),not_homomorphism1(O2::'a,P2,Q2))) &   \
 \  (! R2 T2 S2 U2. equal(R2::'a,S2) --> equal(not_homomorphism1(T2::'a,R2,U2),not_homomorphism1(T2::'a,S2,U2))) &   \
 \  (! V2 X2 Y2 W2. equal(V2::'a,W2) --> equal(not_homomorphism1(X2::'a,Y2,V2),not_homomorphism1(X2::'a,Y2,W2))) &   \
@@ -2062,9 +2067,9 @@
 \  (subclass(domain_relation::'a,cross_product(universal_class::'a,universal_class))) & \
 \  (! X Y. member(ordered_pair(X::'a,Y),domain_relation) --> equal(domain_of(X),Y)) &       \
 \  (! X. member(X::'a,universal_class) --> member(ordered_pair(X::'a,domain_of(X)),domain_relation)) &  \
-\  (! X. equal(first(not_subclass_element(compos(X::'a,inverse(X)),identity_relation)),single_valued1(X))) &       \
-\  (! X. equal(second(not_subclass_element(compos(X::'a,inverse(X)),identity_relation)),single_valued2(X))) &      \
-\  (! X. equal(domain(X::'a,image_(inverse(X),singleton(single_valued1(X))),single_valued2(X)),single_valued3(X))) & \
+\  (! X. equal(first(not_subclass_element(compos(X::'a,INVERSE(X)),identity_relation)),single_valued1(X))) &       \
+\  (! X. equal(second(not_subclass_element(compos(X::'a,INVERSE(X)),identity_relation)),single_valued2(X))) &      \
+\  (! X. equal(domain(X::'a,image_(INVERSE(X),singleton(single_valued1(X))),single_valued2(X)),single_valued3(X))) & \
 \  (equal(intersection(complement(compos(element_relation::'a,complement(identity_relation))),element_relation),singleton_relation)) &     \
 \  (subclass(application_function::'a,cross_product(universal_class::'a,cross_product(universal_class::'a,universal_class)))) &     \
 \  (! Z Y X. member(ordered_pair(X::'a,ordered_pair(Y::'a,Z)),application_function) --> member(Y::'a,domain_of(X))) &       \
@@ -2081,15 +2086,15 @@
 \  (! X2 Y2 Z2 A3. equal(X2::'a,Y2) & maps(X2::'a,Z2,A3) --> maps(Y2::'a,Z2,A3)) &  \
 \  (! B3 D3 C3 E3. equal(B3::'a,C3) & maps(D3::'a,B3,E3) --> maps(D3::'a,C3,E3)) &  \
 \  (! F3 H3 I3 G3. equal(F3::'a,G3) & maps(H3::'a,I3,F3) --> maps(H3::'a,I3,G3)) &  \
-\  (! X. equal(union(X::'a,inverse(X)),symmetrization_of(X))) &     \
+\  (! X. equal(union(X::'a,INVERSE(X)),symmetrization_of(X))) &     \
 \  (! X Y. irreflexive(X::'a,Y) --> subclass(restrct(X::'a,Y,Y),complement(identity_relation))) &      \
 \  (! X Y. subclass(restrct(X::'a,Y,Y),complement(identity_relation)) --> irreflexive(X::'a,Y)) &      \
 \  (! Y X. connected(X::'a,Y) --> subclass(cross_product(Y::'a,Y),union(identity_relation::'a,symmetrization_of(X)))) &     \
 \  (! X Y. subclass(cross_product(Y::'a,Y),union(identity_relation::'a,symmetrization_of(X))) --> connected(X::'a,Y)) &     \
 \  (! Xr Y. transitive(Xr::'a,Y) --> subclass(compos(restrct(Xr::'a,Y,Y),restrct(Xr::'a,Y,Y)),restrct(Xr::'a,Y,Y))) &       \
 \  (! Xr Y. subclass(compos(restrct(Xr::'a,Y,Y),restrct(Xr::'a,Y,Y)),restrct(Xr::'a,Y,Y)) --> transitive(Xr::'a,Y)) &       \
-\  (! Xr Y. asymmetric(Xr::'a,Y) --> equal(restrct(intersection(Xr::'a,inverse(Xr)),Y,Y),null_class)) &        \
-\  (! Xr Y. equal(restrct(intersection(Xr::'a,inverse(Xr)),Y,Y),null_class) --> asymmetric(Xr::'a,Y)) &        \
+\  (! Xr Y. asymmetric(Xr::'a,Y) --> equal(restrct(intersection(Xr::'a,INVERSE(Xr)),Y,Y),null_class)) &        \
+\  (! Xr Y. equal(restrct(intersection(Xr::'a,INVERSE(Xr)),Y,Y),null_class) --> asymmetric(Xr::'a,Y)) &        \
 \  (! Xr Y Z. equal(segment(Xr::'a,Y,Z),domain_of(restrct(Xr::'a,Y,singleton(Z))))) &  \
 \  (! X Y. well_ordering(X::'a,Y) --> connected(X::'a,Y)) &     \
 \  (! Y Xr U. well_ordering(Xr::'a,Y) & subclass(U::'a,Y) --> equal(U::'a,null_class) | member(least(Xr::'a,U),U)) &   \
@@ -2187,11 +2192,11 @@
 (*190 inferences so far.  Searching to depth 10.  0.6 secs*)
 val PLA006_1 = prove
  ("(! X Y State. holds(X::'a,State) & holds(Y::'a,State) --> holds(and'(X::'a,Y),State)) &  \
-\  (! State X. holds(empty::'a,State) & holds(clear(X),State) & differ(X::'a,table) --> holds(holding(X),do(pickup(X),State))) &        \
-\  (! Y X State. holds(on(X::'a,Y),State) & holds(clear(X),State) & holds(empty::'a,State) --> holds(clear(Y),do(pickup(X),State))) &   \
+\  (! State X. holds(EMPTY::'a,State) & holds(clear(X),State) & differ(X::'a,table) --> holds(holding(X),do(pickup(X),State))) &        \
+\  (! Y X State. holds(on(X::'a,Y),State) & holds(clear(X),State) & holds(EMPTY::'a,State) --> holds(clear(Y),do(pickup(X),State))) &   \
 \  (! Y State X Z. holds(on(X::'a,Y),State) & differ(X::'a,Z) --> holds(on(X::'a,Y),do(pickup(Z),State))) & \
 \  (! State X Z. holds(clear(X),State) & differ(X::'a,Z) --> holds(clear(X),do(pickup(Z),State))) & \
-\  (! X Y State. holds(holding(X),State) & holds(clear(Y),State) --> holds(empty::'a,do(putdown(X::'a,Y),State))) &     \
+\  (! X Y State. holds(holding(X),State) & holds(clear(Y),State) --> holds(EMPTY::'a,do(putdown(X::'a,Y),State))) &     \
 \  (! X Y State. holds(holding(X),State) & holds(clear(Y),State) --> holds(on(X::'a,Y),do(putdown(X::'a,Y),State))) &   \
 \  (! X Y State. holds(holding(X),State) & holds(clear(Y),State) --> holds(clear(X),do(putdown(X::'a,Y),State))) &  \
 \  (! Z W X Y State. holds(on(X::'a,Y),State) --> holds(on(X::'a,Y),do(putdown(Z::'a,W),State))) &  \
@@ -2214,7 +2219,7 @@
 \  (holds(clear(a),s0)) &       \
 \  (holds(clear(b),s0)) &       \
 \  (holds(clear(c),s0)) &       \
-\  (holds(empty::'a,s0)) &  \
+\  (holds(EMPTY::'a,s0)) &  \
 \  (! State. holds(clear(table),State)) &       \
 \  (! State. ~holds(on(c::'a,table),State)) --> False",
   meson_tac 1);
@@ -2222,11 +2227,11 @@
 (*190 inferences so far.  Searching to depth 10.  0.5 secs*)
 val PLA017_1 = prove
  ("(! X Y State. holds(X::'a,State) & holds(Y::'a,State) --> holds(and'(X::'a,Y),State)) &  \
-\  (! State X. holds(empty::'a,State) & holds(clear(X),State) & differ(X::'a,table) --> holds(holding(X),do(pickup(X),State))) &        \
-\  (! Y X State. holds(on(X::'a,Y),State) & holds(clear(X),State) & holds(empty::'a,State) --> holds(clear(Y),do(pickup(X),State))) &   \
+\  (! State X. holds(EMPTY::'a,State) & holds(clear(X),State) & differ(X::'a,table) --> holds(holding(X),do(pickup(X),State))) &        \
+\  (! Y X State. holds(on(X::'a,Y),State) & holds(clear(X),State) & holds(EMPTY::'a,State) --> holds(clear(Y),do(pickup(X),State))) &   \
 \  (! Y State X Z. holds(on(X::'a,Y),State) & differ(X::'a,Z) --> holds(on(X::'a,Y),do(pickup(Z),State))) & \
 \  (! State X Z. holds(clear(X),State) & differ(X::'a,Z) --> holds(clear(X),do(pickup(Z),State))) & \
-\  (! X Y State. holds(holding(X),State) & holds(clear(Y),State) --> holds(empty::'a,do(putdown(X::'a,Y),State))) &     \
+\  (! X Y State. holds(holding(X),State) & holds(clear(Y),State) --> holds(EMPTY::'a,do(putdown(X::'a,Y),State))) &     \
 \  (! X Y State. holds(holding(X),State) & holds(clear(Y),State) --> holds(on(X::'a,Y),do(putdown(X::'a,Y),State))) &   \
 \  (! X Y State. holds(holding(X),State) & holds(clear(Y),State) --> holds(clear(X),do(putdown(X::'a,Y),State))) &  \
 \  (! Z W X Y State. holds(on(X::'a,Y),State) --> holds(on(X::'a,Y),do(putdown(Z::'a,W),State))) &  \
@@ -2249,7 +2254,7 @@
 \  (holds(clear(a),s0)) &       \
 \  (holds(clear(b),s0)) &       \
 \  (holds(clear(c),s0)) &       \
-\  (holds(empty::'a,s0)) &  \
+\  (holds(EMPTY::'a,s0)) &  \
 \  (! State. holds(clear(table),State)) &       \
 \  (! State. ~holds(on(a::'a,c),State)) --> False",
   meson_tac 1);
@@ -2257,11 +2262,11 @@
 (*13732 inferences so far.  Searching to depth 16.  9.8 secs*)
 val PLA022_1 = prove_hard
  ("(! X Y State. holds(X::'a,State) & holds(Y::'a,State) --> holds(and'(X::'a,Y),State)) &  \
-\  (! State X. holds(empty::'a,State) & holds(clear(X),State) & differ(X::'a,table) --> holds(holding(X),do(pickup(X),State))) &        \
-\  (! Y X State. holds(on(X::'a,Y),State) & holds(clear(X),State) & holds(empty::'a,State) --> holds(clear(Y),do(pickup(X),State))) &   \
+\  (! State X. holds(EMPTY::'a,State) & holds(clear(X),State) & differ(X::'a,table) --> holds(holding(X),do(pickup(X),State))) &        \
+\  (! Y X State. holds(on(X::'a,Y),State) & holds(clear(X),State) & holds(EMPTY::'a,State) --> holds(clear(Y),do(pickup(X),State))) &   \
 \  (! Y State X Z. holds(on(X::'a,Y),State) & differ(X::'a,Z) --> holds(on(X::'a,Y),do(pickup(Z),State))) & \
 \  (! State X Z. holds(clear(X),State) & differ(X::'a,Z) --> holds(clear(X),do(pickup(Z),State))) & \
-\  (! X Y State. holds(holding(X),State) & holds(clear(Y),State) --> holds(empty::'a,do(putdown(X::'a,Y),State))) &     \
+\  (! X Y State. holds(holding(X),State) & holds(clear(Y),State) --> holds(EMPTY::'a,do(putdown(X::'a,Y),State))) &     \
 \  (! X Y State. holds(holding(X),State) & holds(clear(Y),State) --> holds(on(X::'a,Y),do(putdown(X::'a,Y),State))) &   \
 \  (! X Y State. holds(holding(X),State) & holds(clear(Y),State) --> holds(clear(X),do(putdown(X::'a,Y),State))) &  \
 \  (! Z W X Y State. holds(on(X::'a,Y),State) --> holds(on(X::'a,Y),do(putdown(Z::'a,W),State))) &  \
@@ -2284,7 +2289,7 @@
 \  (holds(clear(a),s0)) &       \
 \  (holds(clear(b),s0)) &       \
 \  (holds(clear(c),s0)) &       \
-\  (holds(empty::'a,s0)) &  \
+\  (holds(EMPTY::'a,s0)) &  \
 \  (! State. holds(clear(table),State)) &       \
 \  (! State. ~holds(and'(on(c::'a,d),on(a::'a,c)),State)) --> False",
   meson_tac 1);
@@ -2292,11 +2297,11 @@
 (*217 inferences so far.  Searching to depth 13.  0.7 secs*)
 val PLA022_2 = prove
  ("(! X Y State. holds(X::'a,State) & holds(Y::'a,State) --> holds(and'(X::'a,Y),State)) &  \
-\  (! State X. holds(empty::'a,State) & holds(clear(X),State) & differ(X::'a,table) --> holds(holding(X),do(pickup(X),State))) &        \
-\  (! Y X State. holds(on(X::'a,Y),State) & holds(clear(X),State) & holds(empty::'a,State) --> holds(clear(Y),do(pickup(X),State))) &   \
+\  (! State X. holds(EMPTY::'a,State) & holds(clear(X),State) & differ(X::'a,table) --> holds(holding(X),do(pickup(X),State))) &        \
+\  (! Y X State. holds(on(X::'a,Y),State) & holds(clear(X),State) & holds(EMPTY::'a,State) --> holds(clear(Y),do(pickup(X),State))) &   \
 \  (! Y State X Z. holds(on(X::'a,Y),State) & differ(X::'a,Z) --> holds(on(X::'a,Y),do(pickup(Z),State))) & \
 \  (! State X Z. holds(clear(X),State) & differ(X::'a,Z) --> holds(clear(X),do(pickup(Z),State))) & \
-\  (! X Y State. holds(holding(X),State) & holds(clear(Y),State) --> holds(empty::'a,do(putdown(X::'a,Y),State))) &     \
+\  (! X Y State. holds(holding(X),State) & holds(clear(Y),State) --> holds(EMPTY::'a,do(putdown(X::'a,Y),State))) &     \
 \  (! X Y State. holds(holding(X),State) & holds(clear(Y),State) --> holds(on(X::'a,Y),do(putdown(X::'a,Y),State))) &   \
 \  (! X Y State. holds(holding(X),State) & holds(clear(Y),State) --> holds(clear(X),do(putdown(X::'a,Y),State))) &  \
 \  (! Z W X Y State. holds(on(X::'a,Y),State) --> holds(on(X::'a,Y),do(putdown(Z::'a,W),State))) &  \
@@ -2319,7 +2324,7 @@
 \  (holds(clear(a),s0)) &       \
 \  (holds(clear(b),s0)) &       \
 \  (holds(clear(c),s0)) &       \
-\  (holds(empty::'a,s0)) &  \
+\  (holds(EMPTY::'a,s0)) &  \
 \  (! State. holds(clear(table),State)) &       \
 \  (! State. ~holds(and'(on(a::'a,c),on(c::'a,d)),State)) --> False",
   meson_tac 1);
@@ -2351,26 +2356,26 @@
 \  (! X. equal(successor(predecessor(X)),X)) &  \
 \  (! X Y. equal(predecessor(X),predecessor(Y)) --> equal(X::'a,Y)) &       \
 \  (! X Y. equal(successor(X),successor(Y)) --> equal(X::'a,Y)) &   \
-\  (! X. less_than(predecessor(X),X)) & \
-\  (! X. less_than(X::'a,successor(X))) &   \
-\  (! X Y Z. less_than(X::'a,Y) & less_than(Y::'a,Z) --> less_than(X::'a,Z)) &      \
-\  (! X Y. less_than(X::'a,Y) | less_than(Y::'a,X) | equal(X::'a,Y)) &    \
-\  (! X. ~less_than(X::'a,X)) &     \
-\  (! Y X. ~(less_than(X::'a,Y) & less_than(Y::'a,X))) &        \
-\  (! Y X Z. equal(X::'a,Y) & less_than(X::'a,Z) --> less_than(Y::'a,Z)) &  \
-\  (! Y Z X. equal(X::'a,Y) & less_than(Z::'a,X) --> less_than(Z::'a,Y)) &  \
+\  (! X. LESS_THAN(predecessor(X),X)) & \
+\  (! X. LESS_THAN(X::'a,successor(X))) &   \
+\  (! X Y Z. LESS_THAN(X::'a,Y) & LESS_THAN(Y::'a,Z) --> LESS_THAN(X::'a,Z)) &      \
+\  (! X Y. LESS_THAN(X::'a,Y) | LESS_THAN(Y::'a,X) | equal(X::'a,Y)) &    \
+\  (! X. ~LESS_THAN(X::'a,X)) &     \
+\  (! Y X. ~(LESS_THAN(X::'a,Y) & LESS_THAN(Y::'a,X))) &        \
+\  (! Y X Z. equal(X::'a,Y) & LESS_THAN(X::'a,Z) --> LESS_THAN(Y::'a,Z)) &  \
+\  (! Y Z X. equal(X::'a,Y) & LESS_THAN(Z::'a,X) --> LESS_THAN(Z::'a,Y)) &  \
 \  (! X Y. equal(X::'a,Y) --> equal(predecessor(X),predecessor(Y))) &       \
 \  (! X Y. equal(X::'a,Y) --> equal(successor(X),successor(Y))) &   \
 \  (! X Y. equal(X::'a,Y) --> equal(a(X),a(Y))) &   \
-\  (~less_than(n::'a,j)) &  \
-\  (less_than(k::'a,j)) &   \
-\  (~less_than(k::'a,i)) &  \
-\  (less_than(i::'a,n)) &   \
-\  (less_than(a(j),a(k))) &     \
-\  (! X. less_than(X::'a,j) & less_than(a(X),a(k)) --> less_than(X::'a,i)) &    \
-\  (! X. less_than(one::'a,i) & less_than(a(X),a(predecessor(i))) --> less_than(X::'a,i) | less_than(n::'a,X)) &   \
-\  (! X. ~(less_than(one::'a,X) & less_than(X::'a,i) & less_than(a(X),a(predecessor(X))))) &    \
-\  (less_than(j::'a,i)) --> False",
+\  (~LESS_THAN(n::'a,j)) &  \
+\  (LESS_THAN(k::'a,j)) &   \
+\  (~LESS_THAN(k::'a,i)) &  \
+\  (LESS_THAN(i::'a,n)) &   \
+\  (LESS_THAN(a(j),a(k))) &     \
+\  (! X. LESS_THAN(X::'a,j) & LESS_THAN(a(X),a(k)) --> LESS_THAN(X::'a,i)) &    \
+\  (! X. LESS_THAN(one::'a,i) & LESS_THAN(a(X),a(predecessor(i))) --> LESS_THAN(X::'a,i) | LESS_THAN(n::'a,X)) &   \
+\  (! X. ~(LESS_THAN(one::'a,X) & LESS_THAN(X::'a,i) & LESS_THAN(a(X),a(predecessor(X))))) &    \
+\  (LESS_THAN(j::'a,i)) --> False",
   meson_tac 1);
 
 (*584 inferences so far.  Searching to depth 7.  1.1 secs*)
@@ -2382,26 +2387,26 @@
 \  (! X. equal(successor(predecessor(X)),X)) &  \
 \  (! X Y. equal(predecessor(X),predecessor(Y)) --> equal(X::'a,Y)) &       \
 \  (! X Y. equal(successor(X),successor(Y)) --> equal(X::'a,Y)) &   \
-\  (! X. less_than(predecessor(X),X)) & \
-\  (! X. less_than(X::'a,successor(X))) &   \
-\  (! X Y Z. less_than(X::'a,Y) & less_than(Y::'a,Z) --> less_than(X::'a,Z)) &      \
-\  (! X Y. less_than(X::'a,Y) | less_than(Y::'a,X) | equal(X::'a,Y)) &    \
-\  (! X. ~less_than(X::'a,X)) &     \
-\  (! Y X. ~(less_than(X::'a,Y) & less_than(Y::'a,X))) &        \
-\  (! Y X Z. equal(X::'a,Y) & less_than(X::'a,Z) --> less_than(Y::'a,Z)) &  \
-\  (! Y Z X. equal(X::'a,Y) & less_than(Z::'a,X) --> less_than(Z::'a,Y)) &  \
+\  (! X. LESS_THAN(predecessor(X),X)) & \
+\  (! X. LESS_THAN(X::'a,successor(X))) &   \
+\  (! X Y Z. LESS_THAN(X::'a,Y) & LESS_THAN(Y::'a,Z) --> LESS_THAN(X::'a,Z)) &      \
+\  (! X Y. LESS_THAN(X::'a,Y) | LESS_THAN(Y::'a,X) | equal(X::'a,Y)) &    \
+\  (! X. ~LESS_THAN(X::'a,X)) &     \
+\  (! Y X. ~(LESS_THAN(X::'a,Y) & LESS_THAN(Y::'a,X))) &        \
+\  (! Y X Z. equal(X::'a,Y) & LESS_THAN(X::'a,Z) --> LESS_THAN(Y::'a,Z)) &  \
+\  (! Y Z X. equal(X::'a,Y) & LESS_THAN(Z::'a,X) --> LESS_THAN(Z::'a,Y)) &  \
 \  (! X Y. equal(X::'a,Y) --> equal(predecessor(X),predecessor(Y))) &       \
 \  (! X Y. equal(X::'a,Y) --> equal(successor(X),successor(Y))) &   \
 \  (! X Y. equal(X::'a,Y) --> equal(a(X),a(Y))) &   \
-\  (~less_than(n::'a,k)) &  \
-\  (~less_than(k::'a,l)) &  \
-\  (~less_than(k::'a,i)) &  \
-\  (less_than(l::'a,n)) &   \
-\  (less_than(one::'a,l)) & \
-\  (less_than(a(k),a(predecessor(l)))) &        \
-\  (! X. less_than(X::'a,successor(n)) & less_than(a(X),a(k)) --> less_than(X::'a,l)) & \
-\  (! X. less_than(one::'a,l) & less_than(a(X),a(predecessor(l))) --> less_than(X::'a,l) | less_than(n::'a,X)) &   \
-\  (! X. ~(less_than(one::'a,X) & less_than(X::'a,l) & less_than(a(X),a(predecessor(X))))) --> False",
+\  (~LESS_THAN(n::'a,k)) &  \
+\  (~LESS_THAN(k::'a,l)) &  \
+\  (~LESS_THAN(k::'a,i)) &  \
+\  (LESS_THAN(l::'a,n)) &   \
+\  (LESS_THAN(one::'a,l)) & \
+\  (LESS_THAN(a(k),a(predecessor(l)))) &        \
+\  (! X. LESS_THAN(X::'a,successor(n)) & LESS_THAN(a(X),a(k)) --> LESS_THAN(X::'a,l)) & \
+\  (! X. LESS_THAN(one::'a,l) & LESS_THAN(a(X),a(predecessor(l))) --> LESS_THAN(X::'a,l) | LESS_THAN(n::'a,X)) &   \
+\  (! X. ~(LESS_THAN(one::'a,X) & LESS_THAN(X::'a,l) & LESS_THAN(a(X),a(predecessor(X))))) --> False",
   meson_tac 1);
 
 (*2343 inferences so far.  Searching to depth 8.  3.5 secs*)
@@ -2413,25 +2418,25 @@
 \  (! X. equal(successor(predecessor(X)),X)) &  \
 \  (! X Y. equal(predecessor(X),predecessor(Y)) --> equal(X::'a,Y)) &       \
 \  (! X Y. equal(successor(X),successor(Y)) --> equal(X::'a,Y)) &   \
-\  (! X. less_than(predecessor(X),X)) & \
-\  (! X. less_than(X::'a,successor(X))) &   \
-\  (! X Y Z. less_than(X::'a,Y) & less_than(Y::'a,Z) --> less_than(X::'a,Z)) &      \
-\  (! X Y. less_than(X::'a,Y) | less_than(Y::'a,X) | equal(X::'a,Y)) &    \
-\  (! X. ~less_than(X::'a,X)) &     \
-\  (! Y X. ~(less_than(X::'a,Y) & less_than(Y::'a,X))) &        \
-\  (! Y X Z. equal(X::'a,Y) & less_than(X::'a,Z) --> less_than(Y::'a,Z)) &  \
-\  (! Y Z X. equal(X::'a,Y) & less_than(Z::'a,X) --> less_than(Z::'a,Y)) &  \
+\  (! X. LESS_THAN(predecessor(X),X)) & \
+\  (! X. LESS_THAN(X::'a,successor(X))) &   \
+\  (! X Y Z. LESS_THAN(X::'a,Y) & LESS_THAN(Y::'a,Z) --> LESS_THAN(X::'a,Z)) &      \
+\  (! X Y. LESS_THAN(X::'a,Y) | LESS_THAN(Y::'a,X) | equal(X::'a,Y)) &    \
+\  (! X. ~LESS_THAN(X::'a,X)) &     \
+\  (! Y X. ~(LESS_THAN(X::'a,Y) & LESS_THAN(Y::'a,X))) &        \
+\  (! Y X Z. equal(X::'a,Y) & LESS_THAN(X::'a,Z) --> LESS_THAN(Y::'a,Z)) &  \
+\  (! Y Z X. equal(X::'a,Y) & LESS_THAN(Z::'a,X) --> LESS_THAN(Z::'a,Y)) &  \
 \  (! X Y. equal(X::'a,Y) --> equal(predecessor(X),predecessor(Y))) &       \
 \  (! X Y. equal(X::'a,Y) --> equal(successor(X),successor(Y))) &   \
 \  (! X Y. equal(X::'a,Y) --> equal(a(X),a(Y))) &   \
-\  (~less_than(n::'a,m)) &  \
-\  (less_than(i::'a,m)) &   \
-\  (less_than(i::'a,n)) &   \
-\  (~less_than(i::'a,one)) &        \
-\  (less_than(a(i),a(m))) &     \
-\  (! X. less_than(X::'a,successor(n)) & less_than(a(X),a(m)) --> less_than(X::'a,i)) & \
-\  (! X. less_than(one::'a,i) & less_than(a(X),a(predecessor(i))) --> less_than(X::'a,i) | less_than(n::'a,X)) &   \
-\  (! X. ~(less_than(one::'a,X) & less_than(X::'a,i) & less_than(a(X),a(predecessor(X))))) --> False",
+\  (~LESS_THAN(n::'a,m)) &  \
+\  (LESS_THAN(i::'a,m)) &   \
+\  (LESS_THAN(i::'a,n)) &   \
+\  (~LESS_THAN(i::'a,one)) &        \
+\  (LESS_THAN(a(i),a(m))) &     \
+\  (! X. LESS_THAN(X::'a,successor(n)) & LESS_THAN(a(X),a(m)) --> LESS_THAN(X::'a,i)) & \
+\  (! X. LESS_THAN(one::'a,i) & LESS_THAN(a(X),a(predecessor(i))) --> LESS_THAN(X::'a,i) | LESS_THAN(n::'a,X)) &   \
+\  (! X. ~(LESS_THAN(one::'a,X) & LESS_THAN(X::'a,i) & LESS_THAN(a(X),a(predecessor(X))))) --> False",
   meson_tac 1);
 
 (*86 inferences so far.  Searching to depth 14.  0.1 secs*)

--- a/src/HOL/mono.ML	Tue Jul 24 11:25:54 2001 +0200
+++ b/src/HOL/mono.ML	Wed Jul 25 13:13:01 2001 +0200
@@ -104,17 +104,6 @@
 val basic_monos = [subset_refl, imp_refl, disj_mono, conj_mono, 
                    ex_mono, Collect_mono, in_mono];
 
-(* Courtesy of Stephan Merz *)
-Goalw [Least_def] 
-"[| mono (f::'a::order => 'b::order); ? x:S. ! y:S. x <= y |] \
-\  ==> (LEAST y. y : f`S) = f(LEAST x. x : S)";
-by (Clarify_tac 1);
-by (eres_inst_tac [("P","%x. x : S")] LeastMI2 1);
-by  (Fast_tac 1);
-by (rtac LeastMI2 1);
-by (auto_tac (claset() addEs [monoD] addSIs [thm "order_antisym"], simpset()));
-qed "Least_mono";
-
 Goal "[| a = b; c = d; b --> d |] ==> a --> c";
 by (Fast_tac 1);
 qed "eq_to_mono";

--- a/src/HOL/simpdata.ML	Tue Jul 24 11:25:54 2001 +0200
+++ b/src/HOL/simpdata.ML	Wed Jul 25 13:13:01 2001 +0200
@@ -96,17 +96,6 @@
                  "(ALL x. P --> Q x) = (P --> (ALL x. Q x))"];
 
 
-(* elimination of existential quantifiers in assumptions *)
-
-val ex_all_equiv =
-  let val lemma1 = prove_goal (the_context ())
-        "(? x. P(x) ==> PROP Q) ==> (!!x. P(x) ==> PROP Q)"
-        (fn prems => [resolve_tac prems 1, etac exI 1]);
-      val lemma2 = prove_goalw (the_context ()) [Ex_def]
-        "(!!x. P(x) ==> PROP Q) ==> (? x. P(x) ==> PROP Q)"
-        (fn prems => [(REPEAT(resolve_tac prems 1))])
-  in equal_intr lemma1 lemma2 end;
-
 end;
 
 bind_thms ("ex_simps", ex_simps);
@@ -391,7 +380,7 @@
        if_True, if_False, if_cancel, if_eq_cancel,
        imp_disjL, conj_assoc, disj_assoc,
        de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, not_imp,
-       disj_not1, not_all, not_ex, cases_simp, some_eq_trivial, some_sym_eq_trivial,
+       disj_not1, not_all, not_ex, cases_simp,
        thm "the_eq_trivial", the_sym_eq_trivial, thm "plus_ac0.zero", thm "plus_ac0_zero_right"]
      @ ex_simps @ all_simps @ simp_thms)
      addsimprocs [defALL_regroup,defEX_regroup]