# HG changeset patch
# User paulson
# Date 1013593709 -3600
# Node ID 75ca1bf5ae122fd5e63b7ebc539759c2b1148b80
# Parent  6288ebcb16233115ab5c79c9e5d90f70f327bf54
deleted some redundant 'addS*Es [equalityC*E]'s

diff -r 6288ebcb1623 -r 75ca1bf5ae12 src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Wed Feb 13 10:45:08 2002 +0100
+++ b/src/HOL/Fun.ML	Wed Feb 13 10:48:29 2002 +0100
@@ -283,7 +283,7 @@
 qed "inj_image_subset_iff";
 
 Goal "inj f ==> (f`A = f`B) = (A = B)";
-by (blast_tac (claset() addSEs [equalityE] addDs [injD]) 1);
+by (blast_tac (claset() addDs [injD]) 1);
 qed "inj_image_eq_iff";
 
 Goal  "(f ` (UNION A B)) = (UN x:A.(f ` (B x)))";
diff -r 6288ebcb1623 -r 75ca1bf5ae12 src/HOL/IOA/IOA.ML
--- a/src/HOL/IOA/IOA.ML	Wed Feb 13 10:45:08 2002 +0100
+++ b/src/HOL/IOA/IOA.ML	Wed Feb 13 10:48:29 2002 +0100
@@ -157,13 +157,13 @@
 Goalw [externals_def,actions_def,compat_ioas_def,compat_asigs_def]
  "[| compat_ioas A1 A2; a:externals(asig_of(A1))|] ==> a~:internals(asig_of(A2))";
 by (Asm_full_simp_tac 1);
-by (best_tac (claset() addEs [equalityCE]) 1);
+by (Best_tac 1);
 qed"ext1_is_not_int2";
 
 Goalw [externals_def,actions_def,compat_ioas_def,compat_asigs_def]
  "[| compat_ioas A2 A1 ; a:externals(asig_of(A1))|] ==> a~:internals(asig_of(A2))";
 by (Asm_full_simp_tac 1);
-by (best_tac (claset() addEs [equalityCE]) 1);
+by (Best_tac 1);
 qed"ext2_is_not_int1";
 
 val ext1_ext2_is_not_act2 = ext1_is_not_int2 RS int_and_ext_is_act;
diff -r 6288ebcb1623 -r 75ca1bf5ae12 src/HOL/Real/PReal.ML
--- a/src/HOL/Real/PReal.ML	Wed Feb 13 10:45:08 2002 +0100
+++ b/src/HOL/Real/PReal.ML	Wed Feb 13 10:48:29 2002 +0100
@@ -115,7 +115,7 @@
 Goal "{xa::prat. xa < y} : preal";
 by (cut_facts_tac [qless_Ex] 1);
 by (auto_tac (claset() addIs[prat_less_trans]
-                       addSEs [equalityCE, prat_less_irrefl], 
+                       addSEs [prat_less_irrefl], 
 	      simpset()));
 by (blast_tac (claset() addDs [prat_dense]) 1);
 qed "lemma_prat_less_set_mem_preal";
@@ -125,8 +125,7 @@
 by Auto_tac;
 by (dtac prat_dense 2 THEN etac exE 2);
 by (dtac prat_dense 1 THEN etac exE 1);
-by (auto_tac (claset() addDs [prat_less_not_sym] addSEs [equalityCE],
-              simpset()));
+by (auto_tac (claset() addDs [prat_less_not_sym], simpset()));
 qed "lemma_prat_set_eq";
 
 Goal "inj(preal_of_prat)";
@@ -204,7 +203,7 @@
 (** Part 1 of Dedekind sections def **)
 Goal "{} < {w. EX x: Rep_preal R. EX y:Rep_preal S. w = x + y}";
 by (cut_facts_tac [mem_Rep_preal_Ex,mem_Rep_preal_Ex] 1);
-by (auto_tac (claset() addSIs [psubsetI] addEs [equalityCE],simpset()));
+by (auto_tac (claset() addSIs [psubsetI], simpset()));
 qed "preal_add_set_not_empty";
 
 (** Part 2 of Dedekind sections def **)
@@ -222,8 +221,6 @@
 Goal "{w. EX x: Rep_preal R. EX y:Rep_preal S. w = x + y} < UNIV";
 by (auto_tac (claset() addSIs [psubsetI],simpset()));
 by (cut_inst_tac [("R","R"),("S","S")] preal_not_mem_add_set_Ex 1);
-by (etac exE 1);
-by (eres_inst_tac [("c","q")] equalityCE 1);
 by Auto_tac;
 qed "preal_add_set_not_prat_set";
 
@@ -292,7 +289,7 @@
 (** Part 1 of Dedekind sections def **)
 Goal "{} < {w. EX x: Rep_preal R. EX y:Rep_preal S. w = x * y}";
 by (cut_facts_tac [mem_Rep_preal_Ex,mem_Rep_preal_Ex] 1);
-by (auto_tac (claset() addSIs [psubsetI] addEs [equalityCE],simpset()));
+by (auto_tac (claset() addSIs [psubsetI], simpset()));
 qed "preal_mult_set_not_empty";
 
 (** Part 2 of Dedekind sections def **)
@@ -310,8 +307,6 @@
 Goal "{w. EX x: Rep_preal R. EX y:Rep_preal S. w = x * y} < UNIV";
 by (auto_tac (claset() addSIs [psubsetI],simpset()));
 by (cut_inst_tac [("R","R"),("S","S")] preal_not_mem_mult_set_Ex 1);
-by (etac exE 1);
-by (eres_inst_tac [("c","q")] equalityCE 1);
 by Auto_tac;
 qed "preal_mult_set_not_prat_set";
 
@@ -509,7 +504,7 @@
 (** Part 1 of Dedekind sections def **)
 Goal "{} < {x. EX y. x < y & qinv y ~:  Rep_preal A}";
 by (cut_facts_tac [lemma_preal_mem_inv_set_ex] 1);
-by (auto_tac (claset() addSIs [psubsetI] addEs [equalityCE],simpset()));
+by (auto_tac (claset() addSIs [psubsetI], simpset()));
 qed "preal_inv_set_not_empty";
 
 (** Part 2 of Dedekind sections def **)
@@ -533,8 +528,6 @@
 Goal "{x. EX y. x < y & qinv y ~:  Rep_preal A} < UNIV";
 by (auto_tac (claset() addSIs [psubsetI],simpset()));
 by (cut_inst_tac [("A","A")]  preal_not_mem_inv_set_Ex 1);
-by (etac exE 1);
-by (eres_inst_tac [("c","x")] equalityCE 1);
 by Auto_tac;
 qed "preal_inv_set_not_prat_set";
 
@@ -831,7 +824,7 @@
 
 Goal "A < B ==> {} < {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
 by (dtac lemma_ex_mem_less_left_add1 1);
-by (auto_tac (claset() addSIs [psubsetI] addEs [equalityCE],simpset()));
+by (auto_tac (claset() addSIs [psubsetI], simpset()));
 qed "preal_less_set_not_empty";
 
 (** Part 2 of Dedekind sections def **)
@@ -847,8 +840,6 @@
 Goal "{d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)} < UNIV";
 by (auto_tac (claset() addSIs [psubsetI],simpset()));
 by (cut_inst_tac [("A","A"),("B","B")] lemma_ex_not_mem_less_left_add1 1);
-by (etac exE 1);
-by (eres_inst_tac [("c","q")] equalityCE 1);
 by Auto_tac;
 qed "preal_less_set_not_prat_set";
 
@@ -1059,7 +1050,7 @@
 Goal "EX (X::preal). X: P ==> \
 \         {} < {w. EX X : P. w : Rep_preal X}";
 by (dtac preal_sup_mem_Ex 1);
-by (auto_tac (claset() addSIs [psubsetI] addEs [equalityCE],simpset()));
+by (auto_tac (claset() addSIs [psubsetI], simpset()));
 qed "preal_sup_set_not_empty";
 
 (** Part 2 of Dedekind sections def **) 
diff -r 6288ebcb1623 -r 75ca1bf5ae12 src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Wed Feb 13 10:45:08 2002 +0100
+++ b/src/HOL/equalities.ML	Wed Feb 13 10:48:29 2002 +0100
@@ -68,7 +68,7 @@
 qed "insert_is_Un";
 
 Goal "insert a A ~= {}";
-by (blast_tac (claset() addEs [equalityCE]) 1);
+by (Blast_tac 1);
 qed"insert_not_empty";
 Addsimps[insert_not_empty];
 
@@ -136,7 +136,7 @@
 Addsimps [insert_image];
 
 Goal "(f`A = {}) = (A = {})";
-by (blast_tac (claset() addSEs [equalityCE]) 1);
+by (Blast_tac 1);
 qed "image_is_empty";
 AddIffs [image_is_empty];
 
@@ -216,7 +216,7 @@
 Addsimps[Int_empty_right];
 
 Goal "(A Int B = {}) = (A <= -B)";
-by (blast_tac (claset() addSEs [equalityCE]) 1);
+by (Blast_tac 1);
 qed "disjoint_eq_subset_Compl";
 
 Goal "(A Int B = {}) = (ALL x:A. ALL y:B. x ~= y)";
@@ -246,7 +246,7 @@
 qed "Int_Un_distrib2";
 
 Goal "(A Int B = UNIV) = (A = UNIV & B = UNIV)";
-by (blast_tac (claset() addEs [equalityCE]) 1);
+by (Blast_tac 1);
 qed "Int_UNIV";
 Addsimps[Int_UNIV];
 
@@ -352,11 +352,11 @@
 qed "Un_Int_crazy";
 
 Goal "(A<=B) = (A Un B = B)";
-by (blast_tac (claset() addSEs [equalityCE]) 1);
+by (Blast_tac 1);
 qed "subset_Un_eq";
 
 Goal "(A Un B = {}) = (A = {} & B = {})";
-by (blast_tac (claset() addEs [equalityCE]) 1);
+by (Blast_tac 1);
 qed "Un_empty";
 AddIffs[Un_empty];
 
@@ -413,7 +413,7 @@
 
 (*Halmos, Naive Set Theory, page 16.*)
 Goal "((A Int B) Un C = A Int (B Un C)) = (C<=A)";
-by (blast_tac (claset() addSEs [equalityCE]) 1);
+by (Blast_tac 1);
 qed "Un_Int_assoc_eq";
 
 Goal "-UNIV = {}";
@@ -469,7 +469,7 @@
 AddIffs [Union_empty_conv];
 
 Goal "(Union(C) Int A = {}) = (ALL B:C. B Int A = {})";
-by (blast_tac (claset() addSEs [equalityCE]) 1);
+by (Blast_tac 1);
 qed "Union_disjoint";
 
 section "Inter";