src/ZF/Epsilon.ML
changeset 6163 be8234f37e48
parent 6071 1b2392ac5752
child 8127 68c6159440f1
     1.1 --- a/src/ZF/Epsilon.ML	Fri Jan 29 16:26:12 1999 +0100
     1.2 +++ b/src/ZF/Epsilon.ML	Fri Jan 29 17:08:20 1999 +0100
     1.3 @@ -217,8 +217,8 @@
     1.4  Goal "rank(Pow(a)) = succ(rank(a))";
     1.5  by (rtac (rank RS trans) 1);
     1.6  by (rtac le_anti_sym 1);
     1.7 -br UN_upper_le 2;
     1.8 -br UN_least_le 1;
     1.9 +by (rtac UN_upper_le 2);
    1.10 +by (rtac UN_least_le 1);
    1.11  by (auto_tac (claset() addIs [rank_mono], simpset()));
    1.12  qed "rank_Pow";
    1.13