# HG changeset patch
# User paulson
# Date 962273838 -7200
# Node ID 69b71b554e91a3f98739512a78a32ba4ade332fe
# Parent  379b0c3f7c852d1c534456adbbcaf355702ee616
the default equalityCE simplifies proofs

diff -r 379b0c3f7c85 -r 69b71b554e91 src/HOL/Real/PReal.ML
--- a/src/HOL/Real/PReal.ML	Thu Jun 29 12:16:43 2000 +0200
+++ b/src/HOL/Real/PReal.ML	Thu Jun 29 12:17:18 2000 +0200
@@ -1103,27 +1103,21 @@
 by (auto_tac (claset() addSDs [bspec],simpset()));
 qed "preal_sup_not_mem_Ex1";
 
-Goal "EX Y. (ALL X: P. X < Y)  \                                    
-\         ==> {w. EX X: P. w: Rep_preal(X)} < UNIV";       (**)
+Goal "EX Y. (ALL X: P. X < Y) ==> {w. EX X: P. w: Rep_preal(X)} < UNIV"; (**)
 by (dtac preal_sup_not_mem_Ex 1);
 by (auto_tac (claset() addSIs [psubsetI],simpset()));
-by (eres_inst_tac [("c","q")] equalityCE 1);
-by Auto_tac;
 qed "preal_sup_set_not_prat_set";
 
-Goal "EX Y. (ALL X: P. X <= Y)  \
-\         ==> {w. EX X: P. w: Rep_preal(X)} < UNIV";
+Goal "EX Y. (ALL X: P. X <= Y) ==> {w. EX X: P. w: Rep_preal(X)} < UNIV";
 by (dtac preal_sup_not_mem_Ex1 1);
 by (auto_tac (claset() addSIs [psubsetI],simpset()));
-by (eres_inst_tac [("c","q")] equalityCE 1);
-by Auto_tac;
 qed "preal_sup_set_not_prat_set1";
 
 (** Part 3 of Dedekind sections def **)
 Goal "[|EX (X::preal). X: P; EX Y. (ALL X:P. X < Y) |] \              
 \         ==> ALL y: {w. EX X: P. w: Rep_preal X}. \
 \             ALL z. z < y --> z: {w. EX X: P. w: Rep_preal X}";         (**)
-by (auto_tac(claset() addEs [Rep_preal RS prealE_lemma3b],simpset()));
+by (auto_tac(claset() addEs [Rep_preal RS prealE_lemma3b], simpset()));
 qed "preal_sup_set_lemma3";
 
 Goal "[|EX (X::preal). X: P; EX Y. (ALL X:P. X <= Y) |] \