# HG changeset patch
# User oheimb
# Date 902929247 -7200
# Node ID d15a4155b96bda73c6e8c8c8daa73fc7980a8bf2
# Parent  81716d9b2b09c02aff43a68a766ea58b47bd5558
added Eps_eq

diff -r 81716d9b2b09 -r d15a4155b96b src/HOL/HOL.ML
--- 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";