# HG changeset patch
# User paulson
# Date 880561972 -3600
# Node ID ddbe1a9722abd27c630c3d086ddc53483a5054be
# Parent  03d7de40ee4fe56d143524be4335cc01b8d89957
Tidying and using equalityCE instead of the slower equalityE

diff -r 03d7de40ee4f -r ddbe1a9722ab src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Wed Nov 26 17:31:02 1997 +0100
+++ b/src/HOL/equalities.ML	Wed Nov 26 17:32:52 1997 +0100
@@ -105,7 +105,7 @@
 Addsimps [insert_image];
 
 goal thy "(f``A = {}) = (A = {})";
-by (blast_tac (claset() addSEs [equalityE]) 1);
+by (blast_tac (claset() addSEs [equalityCE]) 1);
 qed "image_is_empty";
 AddIffs [image_is_empty];
 
@@ -149,7 +149,7 @@
 Addsimps[Int_empty_right];
 
 goal thy "(A Int B = {}) = (A <= Compl B)";
-by (blast_tac (claset() addSEs [equalityE]) 1);
+by (blast_tac (claset() addSEs [equalityCE]) 1);
 qed "disjoint_eq_subset_Compl";
 
 goal thy "UNIV Int B = B";
@@ -171,7 +171,7 @@
 qed "Int_Un_distrib2";
 
 goal thy "(A<=B) = (A Int B = A)";
-by (blast_tac (claset() addSEs [equalityE]) 1);
+by (blast_tac (claset() addSEs [equalityCE]) 1);
 qed "subset_Int_eq";
 
 goal thy "(A Int B = UNIV) = (A = UNIV & B = UNIV)";
@@ -233,13 +233,13 @@
 Addsimps[Un_insert_right];
 
 goal thy "(insert a B) Int C = (if a:C then insert a (B Int C) \
-\                                          else        B Int C)";
+\                                      else        B Int C)";
 by (simp_tac (simpset() addsplits [expand_if]) 1);
 by (Blast_tac 1);
 qed "Int_insert_left";
 
 goal thy "A Int (insert a B) = (if a:A then insert a (A Int B) \
-\                                          else        A Int B)";
+\                                      else        A Int B)";
 by (simp_tac (simpset() addsplits [expand_if]) 1);
 by (Blast_tac 1);
 qed "Int_insert_right";
@@ -254,7 +254,7 @@
 qed "Un_Int_crazy";
 
 goal thy "(A<=B) = (A Un B = B)";
-by (blast_tac (claset() addSEs [equalityE]) 1);
+by (blast_tac (claset() addSEs [equalityCE]) 1);
 qed "subset_Un_eq";
 
 goal thy "(A <= insert b C) = (A <= C | b:A & A-{b} <= C)";
@@ -301,7 +301,7 @@
 (*Halmos, Naive Set Theory, page 16.*)
 
 goal thy "((A Int B) Un C = A Int (B Un C)) = (C<=A)";
-by (blast_tac (claset() addSEs [equalityE]) 1);
+by (blast_tac (claset() addSEs [equalityCE]) 1);
 qed "Un_Int_assoc_eq";
 
 
@@ -332,12 +332,12 @@
 qed "Union_Int_subset";
 
 goal thy "(Union M = {}) = (! A : M. A = {})"; 
-by (blast_tac (claset() addEs [equalityE]) 1);
-qed"Union_empty_conv"; 
+by (blast_tac (claset() addEs [equalityCE]) 1);
+qed "Union_empty_conv"; 
 AddIffs [Union_empty_conv];
 
 goal thy "(Union(C) Int A = {}) = (! B:C. B Int A = {})";
-by (blast_tac (claset() addSEs [equalityE]) 1);
+by (blast_tac (claset() addSEs [equalityCE]) 1);
 qed "Union_disjoint";
 
 section "Inter";
@@ -444,7 +444,7 @@
 by (Blast_tac 1);
 qed "Int_Union";
 
-(* Devlin, Setdamentals of Contemporary Set Theory, page 12, exercise 5: 
+(* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: 
    Union of a family of unions **)
 goal thy "(UN x:C. A(x) Un B(x)) = Union(A``C)  Un  Union(B``C)";
 by (Blast_tac 1);