src/ZF/ex/Limit.ML
changeset 6163 be8234f37e48
parent 6158 981f96a598f5
child 6169 f3f2560fbed9
     1.1 --- a/src/ZF/ex/Limit.ML	Fri Jan 29 16:26:12 1999 +0100
     1.2 +++ b/src/ZF/ex/Limit.ML	Fri Jan 29 17:08:20 1999 +0100
     1.3 @@ -1425,7 +1425,7 @@
     1.4  
     1.5  Goal "emb_chain(DD,ee) ==> cpo(Dinf(DD,ee))";
     1.6  by (rtac subcpo_cpo 1);
     1.7 -be subcpo_Dinf 1;
     1.8 +by (etac subcpo_Dinf 1);
     1.9  by (auto_tac (claset() addIs [cpo_iprod, emb_chain_cpo], simpset()));
    1.10  qed "cpo_Dinf";
    1.11