Removed equalityI from some proofs (because it is now included
authorberghofe
Thu May 23 15:15:20 1996 +0200 (1996-05-23)
changeset 176129e08d527ba1
parent 1760 6f41a494f3b1
child 1762 6e481897a811
Removed equalityI from some proofs (because it is now included
in the default claset)
src/HOL/Relation.ML
src/HOL/Sum.ML
src/HOL/Univ.ML
src/HOL/subset.ML
     1.1 --- a/src/HOL/Relation.ML	Thu May 23 14:37:06 1996 +0200
     1.2 +++ b/src/HOL/Relation.ML	Thu May 23 15:15:20 1996 +0200
     1.3 @@ -110,7 +110,7 @@
     1.4                            addSEs [converseD,converseE];
     1.5  
     1.6  goalw Relation.thy [converse_def] "converse(converse R) = R";
     1.7 -by(fast_tac (!claset addSIs [equalityI]) 1);
     1.8 +by(Fast_tac 1);
     1.9  qed "converse_converse";
    1.10  
    1.11  (** Domain **)
     2.1 --- a/src/HOL/Sum.ML	Thu May 23 14:37:06 1996 +0200
     2.2 +++ b/src/HOL/Sum.ML	Thu May 23 15:15:20 1996 +0200
     2.3 @@ -204,14 +204,14 @@
     2.4  qed "PartD1";
     2.5  
     2.6  goal Sum.thy "Part A (%x.x) = A";
     2.7 -by (fast_tac (!claset addIs [PartI,equalityI] addSEs [PartE]) 1);
     2.8 +by (fast_tac (!claset addIs [PartI] addSEs [PartE]) 1);
     2.9  qed "Part_id";
    2.10  
    2.11  goal Sum.thy "Part (A Int B) h = (Part A h) Int (Part B h)";
    2.12 -by (fast_tac (!claset addIs [PartI,equalityI] addSEs [PartE]) 1);
    2.13 +by (fast_tac (!claset addIs [PartI] addSEs [PartE]) 1);
    2.14  qed "Part_Int";
    2.15  
    2.16  (*For inductive definitions*)
    2.17  goal Sum.thy "Part (A Int {x.P x}) h = (Part A h) Int {x.P x}";
    2.18 -by (fast_tac (!claset addIs [PartI,equalityI] addSEs [PartE]) 1);
    2.19 +by (fast_tac (!claset addIs [PartI] addSEs [PartE]) 1);
    2.20  qed "Part_Collect";
     3.1 --- a/src/HOL/Univ.ML	Thu May 23 14:37:06 1996 +0200
     3.2 +++ b/src/HOL/Univ.ML	Thu May 23 15:15:20 1996 +0200
     3.3 @@ -430,15 +430,15 @@
     3.4  (**** UN x. B(x) rules ****)
     3.5  
     3.6  goalw Univ.thy [ntrunc_def] "ntrunc k (UN x.f(x)) = (UN x. ntrunc k (f x))";
     3.7 -by (fast_tac (!claset addIs [equalityI]) 1);
     3.8 +by (Fast_tac 1);
     3.9  qed "ntrunc_UN1";
    3.10  
    3.11  goalw Univ.thy [Scons_def] "(UN x.f(x)) $ M = (UN x. f(x) $ M)";
    3.12 -by (fast_tac (!claset addIs [equalityI]) 1);
    3.13 +by (Fast_tac 1);
    3.14  qed "Scons_UN1_x";
    3.15  
    3.16  goalw Univ.thy [Scons_def] "M $ (UN x.f(x)) = (UN x. M $ f(x))";
    3.17 -by (fast_tac (!claset addIs [equalityI]) 1);
    3.18 +by (Fast_tac 1);
    3.19  qed "Scons_UN1_y";
    3.20  
    3.21  goalw Univ.thy [In0_def] "In0(UN x.f(x)) = (UN x. In0(f(x)))";
    3.22 @@ -556,16 +556,16 @@
    3.23  (*** Domain ***)
    3.24  
    3.25  goal Univ.thy "fst `` diag(A) = A";
    3.26 -by (fast_tac (!claset addIs [equalityI, diagI] addSEs [diagE]) 1);
    3.27 +by (fast_tac (!claset addIs [diagI] addSEs [diagE]) 1);
    3.28  qed "fst_image_diag";
    3.29  
    3.30  goal Univ.thy "fst `` (r<**>s) = (fst``r) <*> (fst``s)";
    3.31 -by (fast_tac (!claset addIs [equalityI, uprodI, dprodI]
    3.32 +by (fast_tac (!claset addIs [uprodI, dprodI]
    3.33                       addSEs [uprodE, dprodE]) 1);
    3.34  qed "fst_image_dprod";
    3.35  
    3.36  goal Univ.thy "fst `` (r<++>s) = (fst``r) <+> (fst``s)";
    3.37 -by (fast_tac (!claset addIs [equalityI, usum_In0I, usum_In1I, 
    3.38 +by (fast_tac (!claset addIs [usum_In0I, usum_In1I, 
    3.39                               dsum_In0I, dsum_In1I]
    3.40                       addSEs [usumE, dsumE]) 1);
    3.41  qed "fst_image_dsum";
     4.1 --- a/src/HOL/subset.ML	Thu May 23 14:37:06 1996 +0200
     4.2 +++ b/src/HOL/subset.ML	Thu May 23 15:15:20 1996 +0200
     4.3 @@ -17,7 +17,7 @@
     4.4  qed "subset_insert";
     4.5  
     4.6  qed_goal "subset_empty_iff" Set.thy "(A<={}) = (A={})"
     4.7 - (fn _=> [ (fast_tac (!claset addIs [equalityI]) 1) ]);
     4.8 + (fn _=> [ (Fast_tac 1) ]);
     4.9  
    4.10  (*** Big Union -- least upper bound of a set  ***)
    4.11