src/HOL/Real/PReal.ML
changeset 13849 2584233cf3ef
parent 13624 17684cf64fda
     1.1 --- a/src/HOL/Real/PReal.ML	Thu Mar 06 12:22:28 2003 +0100
     1.2 +++ b/src/HOL/Real/PReal.ML	Thu Mar 06 15:02:51 2003 +0100
     1.3 @@ -122,10 +122,11 @@
     1.4  
     1.5  Goal "!!(x::prat). {xa. xa < x} = {x. x < y} ==> x = y";
     1.6  by (cut_inst_tac [("q1.0","x"),("q2.0","y")] prat_linear 1);
     1.7 -by Auto_tac;
     1.8 +by Safe_tac;
     1.9  by (dtac prat_dense 2 THEN etac exE 2);
    1.10  by (dtac prat_dense 1 THEN etac exE 1);
    1.11 -by (auto_tac (claset() addDs [prat_less_not_sym], simpset()));
    1.12 +by (blast_tac (claset() addDs [prat_less_not_sym]) 1); 
    1.13 +by (blast_tac (claset() addDs [prat_less_not_sym]) 1); 
    1.14  qed "lemma_prat_set_eq";
    1.15  
    1.16  Goal "inj(preal_of_prat)";