src/HOL/Real/PReal.ML
changeset 9189 69b71b554e91
parent 9108 9fff97d29837
child 9266 1b917b8b1b38
     1.1 --- a/src/HOL/Real/PReal.ML	Thu Jun 29 12:16:43 2000 +0200
     1.2 +++ b/src/HOL/Real/PReal.ML	Thu Jun 29 12:17:18 2000 +0200
     1.3 @@ -1103,27 +1103,21 @@
     1.4  by (auto_tac (claset() addSDs [bspec],simpset()));
     1.5  qed "preal_sup_not_mem_Ex1";
     1.6  
     1.7 -Goal "EX Y. (ALL X: P. X < Y)  \                                    
     1.8 -\         ==> {w. EX X: P. w: Rep_preal(X)} < UNIV";       (**)
     1.9 +Goal "EX Y. (ALL X: P. X < Y) ==> {w. EX X: P. w: Rep_preal(X)} < UNIV"; (**)
    1.10  by (dtac preal_sup_not_mem_Ex 1);
    1.11  by (auto_tac (claset() addSIs [psubsetI],simpset()));
    1.12 -by (eres_inst_tac [("c","q")] equalityCE 1);
    1.13 -by Auto_tac;
    1.14  qed "preal_sup_set_not_prat_set";
    1.15  
    1.16 -Goal "EX Y. (ALL X: P. X <= Y)  \
    1.17 -\         ==> {w. EX X: P. w: Rep_preal(X)} < UNIV";
    1.18 +Goal "EX Y. (ALL X: P. X <= Y) ==> {w. EX X: P. w: Rep_preal(X)} < UNIV";
    1.19  by (dtac preal_sup_not_mem_Ex1 1);
    1.20  by (auto_tac (claset() addSIs [psubsetI],simpset()));
    1.21 -by (eres_inst_tac [("c","q")] equalityCE 1);
    1.22 -by Auto_tac;
    1.23  qed "preal_sup_set_not_prat_set1";
    1.24  
    1.25  (** Part 3 of Dedekind sections def **)
    1.26  Goal "[|EX (X::preal). X: P; EX Y. (ALL X:P. X < Y) |] \              
    1.27  \         ==> ALL y: {w. EX X: P. w: Rep_preal X}. \
    1.28  \             ALL z. z < y --> z: {w. EX X: P. w: Rep_preal X}";         (**)
    1.29 -by (auto_tac(claset() addEs [Rep_preal RS prealE_lemma3b],simpset()));
    1.30 +by (auto_tac(claset() addEs [Rep_preal RS prealE_lemma3b], simpset()));
    1.31  qed "preal_sup_set_lemma3";
    1.32  
    1.33  Goal "[|EX (X::preal). X: P; EX Y. (ALL X:P. X <= Y) |] \