author berghofe Thu May 23 15:15:20 1996 +0200 (1996-05-23) changeset 1761 29e08d527ba1 parent 1760 6f41a494f3b1 child 1762 6e481897a811
Removed equalityI from some proofs (because it is now included
in the default claset)
 src/HOL/Relation.ML file | annotate | diff | revisions src/HOL/Sum.ML file | annotate | diff | revisions src/HOL/Univ.ML file | annotate | diff | revisions src/HOL/subset.ML file | annotate | diff | revisions
```     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.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.9  qed "Part_id";
2.10
2.11  goal Sum.thy "Part (A Int B) h = (Part A h) Int (Part B h)";
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.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.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.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.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
```