| changeset 5299 | d15a4155b96b |
| parent 5228 | 66925577cefe |
| child 5309 | 01c2b317da88 |
--- 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";