src/HOL/HOL.ML
changeset 5447 df03d330aeab
parent 5346 bc9748ad8491
child 5760 7e2cf2820684
     1.1 --- a/src/HOL/HOL.ML	Wed Sep 09 17:25:49 1998 +0200
     1.2 +++ b/src/HOL/HOL.ML	Wed Sep 09 17:34:58 1998 +0200
     1.3 @@ -297,7 +297,12 @@
     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 +qed_goal "Eps_eq" HOL.thy "(@y. y=x) = x" (K [
     1.9 +	rtac select_equality 1,
    1.10 +	rtac refl 1,
    1.11 +	atac 1]);
    1.12 +
    1.13 +qed_goal "Eps_sym_eq" HOL.thy "(Eps (op = x)) = x" (K [
    1.14  	rtac select_equality 1,
    1.15  	rtac refl 1,
    1.16  	etac sym 1]);