src/HOL/Relation.ML
changeset 9969 4753185f1dd2
parent 9113 e221d4f81d52
child 10786 04ee73606993
     1.1 --- a/src/HOL/Relation.ML	Fri Sep 15 11:34:46 2000 +0200
     1.2 +++ b/src/HOL/Relation.ML	Fri Sep 15 12:39:57 2000 +0200
     1.3 @@ -442,12 +442,12 @@
     1.4  by (rtac CollectI 1);
     1.5  by (rtac allI 1);
     1.6  by (etac allE 1);
     1.7 -by (rtac (select_eq_Ex RS iffD2) 1);
     1.8 +by (rtac (some_eq_ex RS iffD2) 1);
     1.9  by (etac ex1_implies_ex 1);
    1.10  by (rtac ext 1);
    1.11  by (etac CollectE 1);
    1.12  by (REPEAT (etac allE 1));
    1.13 -by (rtac (select1_equality RS sym) 1);
    1.14 +by (rtac (some1_equality RS sym) 1);
    1.15  by (atac 1);
    1.16  by (atac 1);
    1.17  qed "fun_rel_comp_unique";