added Eps_eq

--- a/src/HOL/HOL.ML	Wed Aug 12 15:38:34 1998 +0200
+++ b/src/HOL/HOL.ML	Wed Aug 12 15:40:47 1998 +0200
@@ -292,6 +292,10 @@
         etac exE 1,
         etac selectI 1]);
 
+qed_goal "Eps_eq" HOL.thy "(Eps (op = x)) = x" (K [
+	rtac select_equality 1,
+	rtac refl 1,
+	etac sym 1]);
 
 (** Classical intro rules for disjunction and existential quantifiers *)
 section "classical intro rules";