# HG changeset patch
# User oheimb
# Date 884278042 -3600
# Node ID 4878fb3d0ac576c20893a8203674e6b3b8ad1be6
# Parent  6be35399125ad3b5ce92d26fa982da7e35689ef1
removed Eps_eq, ex1_Eps_eq, and some unnecessary parentheses

diff -r 6be35399125a -r 4878fb3d0ac5 src/HOL/HOL.ML
--- a/src/HOL/HOL.ML	Thu Jan 08 17:44:50 1998 +0100
+++ b/src/HOL/HOL.ML	Thu Jan 08 17:47:22 1998 +0100
@@ -159,7 +159,7 @@
 (** Existential quantifier **)
 section "?";
 
-qed_goalw "exI" HOL.thy [Ex_def] "P(x) ==> ? x::'a. P(x)"
+qed_goalw "exI" HOL.thy [Ex_def] "P x ==> ? x::'a. P x"
  (fn prems => [rtac selectI 1, resolve_tac prems 1]);
 
 qed_goalw "exE" HOL.thy [Ex_def]
@@ -256,23 +256,23 @@
 
 (*Easier to apply than selectI: conclusion has only one occurrence of P*)
 qed_goal "selectI2" HOL.thy
-    "[| P(a);  !!x. P(x) ==> Q(x) |] ==> Q(@x. P(x))"
+    "[| P a;  !!x. P x ==> Q x |] ==> Q (@x. P x)"
  (fn prems => [ resolve_tac prems 1, 
                 rtac selectI 1, 
                 resolve_tac prems 1 ]);
 
 (*Easier to apply than selectI2 if witness ?a comes from an EX-formula*)
 qed_goal "selectI2EX" HOL.thy
-  "[| ? a. P a; !!x. P x ==> Q x |] ==> Q(Eps P)"
+  "[| ? a. P a; !!x. P x ==> Q x |] ==> Q (Eps P)"
 (fn [major,minor] => [rtac (major RS exE) 1, etac selectI2 1, etac minor 1]);
 
 qed_goal "select_equality" HOL.thy
-    "[| P(a);  !!x. P(x) ==> x=a |] ==> (@x. P(x)) = a"
+    "[| P a;  !!x. P x ==> x=a |] ==> (@x. P x) = a"
  (fn prems => [ rtac selectI2 1, 
                 REPEAT (ares_tac prems 1) ]);
 
 qed_goalw "select1_equality" HOL.thy [Ex1_def]
-  "!!P. [| ?!x. P(x); P(a) |] ==> (@x. P(x)) = a" (K [
+  "!!P. [| ?!x. P x; P a |] ==> (@x. P x) = a" (K [
 	  rtac select_equality 1, atac 1,
           etac exE 1, etac conjE 1,
           rtac allE 1, atac 1,
@@ -286,22 +286,6 @@
         etac exE 1,
         etac selectI 1]);
 
-val Eps_eq = prove_goal HOL.thy "Eps (op = x) = x" (K [
-	rtac select_equality 1, rtac refl 1, etac sym 1]);
-
-val ex1_Eps_eq = prove_goal HOL.thy "!!X. [|?!x. P x; P y|] ==> Eps P = y" (K [
-	rtac select_equality 1,
-	 atac 1,
-	etac ex1E 1,
-	etac all_dupE 1,
-	etac impE 1,
-	 atac 1,
-	rtac trans 1,
-	 etac sym 2,
-	dtac spec 1,
-	etac impE 1,
-	 ALLGOALS atac]);
-
 
 (** Classical intro rules for disjunction and existential quantifiers *)
 section "classical intro rules";