changeset 5447 | df03d330aeab |
parent 5346 | bc9748ad8491 |
child 5760 | 7e2cf2820684 |
--- a/src/HOL/HOL.ML Wed Sep 09 17:25:49 1998 +0200 +++ b/src/HOL/HOL.ML Wed Sep 09 17:34:58 1998 +0200 @@ -297,7 +297,12 @@ etac exE 1, etac selectI 1]); -qed_goal "Eps_eq" HOL.thy "(Eps (op = x)) = x" (K [ +qed_goal "Eps_eq" HOL.thy "(@y. y=x) = x" (K [ + rtac select_equality 1, + rtac refl 1, + atac 1]); + +qed_goal "Eps_sym_eq" HOL.thy "(Eps (op = x)) = x" (K [ rtac select_equality 1, rtac refl 1, etac sym 1]);