# HG changeset patch
# User berghofe
# Date 832857320 -7200
# Node ID 29e08d527ba1852ca2ccc7347c2037cadf9468a9
# Parent  6f41a494f3b153190999435febb947ef2264de34
Removed equalityI from some proofs (because it is now included
in the default claset)

diff -r 6f41a494f3b1 -r 29e08d527ba1 src/HOL/Relation.ML
--- a/src/HOL/Relation.ML	Thu May 23 14:37:06 1996 +0200
+++ b/src/HOL/Relation.ML	Thu May 23 15:15:20 1996 +0200
@@ -110,7 +110,7 @@
                           addSEs [converseD,converseE];
 
 goalw Relation.thy [converse_def] "converse(converse R) = R";
-by(fast_tac (!claset addSIs [equalityI]) 1);
+by(Fast_tac 1);
 qed "converse_converse";
 
 (** Domain **)
diff -r 6f41a494f3b1 -r 29e08d527ba1 src/HOL/Sum.ML
--- a/src/HOL/Sum.ML	Thu May 23 14:37:06 1996 +0200
+++ b/src/HOL/Sum.ML	Thu May 23 15:15:20 1996 +0200
@@ -204,14 +204,14 @@
 qed "PartD1";
 
 goal Sum.thy "Part A (%x.x) = A";
-by (fast_tac (!claset addIs [PartI,equalityI] addSEs [PartE]) 1);
+by (fast_tac (!claset addIs [PartI] addSEs [PartE]) 1);
 qed "Part_id";
 
 goal Sum.thy "Part (A Int B) h = (Part A h) Int (Part B h)";
-by (fast_tac (!claset addIs [PartI,equalityI] addSEs [PartE]) 1);
+by (fast_tac (!claset addIs [PartI] addSEs [PartE]) 1);
 qed "Part_Int";
 
 (*For inductive definitions*)
 goal Sum.thy "Part (A Int {x.P x}) h = (Part A h) Int {x.P x}";
-by (fast_tac (!claset addIs [PartI,equalityI] addSEs [PartE]) 1);
+by (fast_tac (!claset addIs [PartI] addSEs [PartE]) 1);
 qed "Part_Collect";
diff -r 6f41a494f3b1 -r 29e08d527ba1 src/HOL/Univ.ML
--- a/src/HOL/Univ.ML	Thu May 23 14:37:06 1996 +0200
+++ b/src/HOL/Univ.ML	Thu May 23 15:15:20 1996 +0200
@@ -430,15 +430,15 @@
 (**** UN x. B(x) rules ****)
 
 goalw Univ.thy [ntrunc_def] "ntrunc k (UN x.f(x)) = (UN x. ntrunc k (f x))";
-by (fast_tac (!claset addIs [equalityI]) 1);
+by (Fast_tac 1);
 qed "ntrunc_UN1";
 
 goalw Univ.thy [Scons_def] "(UN x.f(x)) $ M = (UN x. f(x) $ M)";
-by (fast_tac (!claset addIs [equalityI]) 1);
+by (Fast_tac 1);
 qed "Scons_UN1_x";
 
 goalw Univ.thy [Scons_def] "M $ (UN x.f(x)) = (UN x. M $ f(x))";
-by (fast_tac (!claset addIs [equalityI]) 1);
+by (Fast_tac 1);
 qed "Scons_UN1_y";
 
 goalw Univ.thy [In0_def] "In0(UN x.f(x)) = (UN x. In0(f(x)))";
@@ -556,16 +556,16 @@
 (*** Domain ***)
 
 goal Univ.thy "fst `` diag(A) = A";
-by (fast_tac (!claset addIs [equalityI, diagI] addSEs [diagE]) 1);
+by (fast_tac (!claset addIs [diagI] addSEs [diagE]) 1);
 qed "fst_image_diag";
 
 goal Univ.thy "fst `` (r<**>s) = (fst``r) <*> (fst``s)";
-by (fast_tac (!claset addIs [equalityI, uprodI, dprodI]
+by (fast_tac (!claset addIs [uprodI, dprodI]
                      addSEs [uprodE, dprodE]) 1);
 qed "fst_image_dprod";
 
 goal Univ.thy "fst `` (r<++>s) = (fst``r) <+> (fst``s)";
-by (fast_tac (!claset addIs [equalityI, usum_In0I, usum_In1I, 
+by (fast_tac (!claset addIs [usum_In0I, usum_In1I, 
                              dsum_In0I, dsum_In1I]
                      addSEs [usumE, dsumE]) 1);
 qed "fst_image_dsum";
diff -r 6f41a494f3b1 -r 29e08d527ba1 src/HOL/subset.ML
--- a/src/HOL/subset.ML	Thu May 23 14:37:06 1996 +0200
+++ b/src/HOL/subset.ML	Thu May 23 15:15:20 1996 +0200
@@ -17,7 +17,7 @@
 qed "subset_insert";
 
 qed_goal "subset_empty_iff" Set.thy "(A<={}) = (A={})"
- (fn _=> [ (fast_tac (!claset addIs [equalityI]) 1) ]);
+ (fn _=> [ (Fast_tac 1) ]);
 
 (*** Big Union -- least upper bound of a set  ***)