src/HOL/HOL.ML
changeset 5299 d15a4155b96b
parent 5228 66925577cefe
child 5309 01c2b317da88
     1.1 --- a/src/HOL/HOL.ML	Wed Aug 12 15:38:34 1998 +0200
     1.2 +++ b/src/HOL/HOL.ML	Wed Aug 12 15:40:47 1998 +0200
     1.3 @@ -292,6 +292,10 @@
     1.4          etac exE 1,
     1.5          etac selectI 1]);
     1.6  
     1.7 +qed_goal "Eps_eq" HOL.thy "(Eps (op = x)) = x" (K [
     1.8 +	rtac select_equality 1,
     1.9 +	rtac refl 1,
    1.10 +	etac sym 1]);
    1.11  
    1.12  (** Classical intro rules for disjunction and existential quantifiers *)
    1.13  section "classical intro rules";