src/HOL/Fun.ML

--- a/src/HOL/Fun.ML	Thu Jan 09 10:22:42 1997 +0100
+++ b/src/HOL/Fun.ML	Thu Jan 09 10:23:39 1997 +0100
@@ -35,14 +35,15 @@
 by (REPEAT (ares_tac prems 1));
 qed "imageE";
 
+AddIs  [imageI]; 
+AddSEs [imageE]; 
+
 goalw Fun.thy [o_def] "(f o g)``r = f``(g``r)";
-by (rtac set_ext 1);
-by (fast_tac (!claset addIs [imageI] addSEs [imageE]) 1);
+by (Fast_tac 1);
 qed "image_compose";
 
 goal Fun.thy "f``(A Un B) = f``A Un f``B";
-by (rtac set_ext 1);
-by (fast_tac (!claset addIs [imageI,UnCI] addSEs [imageE,UnE]) 1);
+by (Fast_tac 1);
 qed "image_Un";
 
 (*** Range of a function -- just a translation for image! ***)
@@ -108,7 +109,7 @@
 
 val prems = goalw Fun.thy [inj_onto_def]
     "(!! x y. [| f(x) = f(y);  x:A;  y:A |] ==> x=y) ==> inj_onto f A";
-by (fast_tac (!claset addIs prems addSIs [ballI]) 1);
+by (fast_tac (!claset addIs prems) 1);
 qed "inj_ontoI";
 
 val [major] = goal Fun.thy 
@@ -141,7 +142,7 @@
 val prems = goalw Fun.thy [o_def]
     "[| inj(f);  inj_onto g (range f) |] ==> inj(g o f)";
 by (cut_facts_tac prems 1);
-by (fast_tac (!claset addIs [injI,rangeI]
+by (fast_tac (!claset addIs [injI]
                      addEs [injD,inj_ontoD]) 1);
 qed "comp_inj";
 
@@ -163,20 +164,12 @@
     "[| inj(f);  A<=range(f) |] ==> inj_onto (Inv f) A";
 by (cut_facts_tac prems 1);
 by (fast_tac (!claset addIs [inj_ontoI] 
-                     addEs [Inv_injective,injD,subsetD]) 1);
+                      addEs [Inv_injective,injD]) 1);
 qed "inj_onto_Inv";
 
 
-(*** Set reasoning tools ***)
-
-AddSIs [ballI, PowI, subsetI, InterI, INT_I, INT1_I, CollectI, 
-            ComplI, IntI, DiffI, UnCI, insertCI]; 
-AddIs  [bexI, UnionI, UN_I, UN1_I, imageI, rangeI]; 
-AddSEs [bexE, make_elim PowD, UnionE, UN_E, UN1_E, DiffE,
-            make_elim singleton_inject,
-            CollectE, ComplE, IntE, UnE, insertE, imageE, rangeE, emptyE]; 
-AddEs  [ballE, InterD, InterE, INT_D, INT_E, make_elim INT1_D,
-            subsetD, subsetCE];
+AddIs  [rangeI]; 
+AddSEs [rangeE]; 
 
 val set_cs = !claset delrules [equalityI];