1.1 --- a/src/HOL/Fun.ML	Tue May 21 10:52:26 1996 +0200
     1.2 +++ b/src/HOL/Fun.ML	Tue May 21 13:39:31 1996 +0200
     1.3 @@ -51,19 +51,19 @@
     1.4  
     1.5  goalw Fun.thy [o_def] "(f o g)``r = f``(g``r)";
     1.6  by (rtac set_ext 1);
     1.7 -by (fast_tac (HOL_cs addIs [imageI] addSEs [imageE]) 1);
     1.8 +by (fast_tac (!claset addIs [imageI] addSEs [imageE]) 1);
     1.9  qed "image_compose";
    1.10  
    1.11  goal Fun.thy "f``(A Un B) = f``A Un f``B";
    1.12  by (rtac set_ext 1);
    1.13 -by (fast_tac (HOL_cs addIs [imageI,UnCI] addSEs [imageE,UnE]) 1);
    1.14 +by (fast_tac (!claset addIs [imageI,UnCI] addSEs [imageE,UnE]) 1);
    1.15  qed "image_Un";
    1.16  
    1.17  (*** inj(f): f is a one-to-one function ***)
    1.18  
    1.19  val prems = goalw Fun.thy [inj_def]
    1.20      "[| !! x y. f(x) = f(y) ==> x=y |] ==> inj(f)";
    1.21 -by (fast_tac (HOL_cs addIs prems) 1);
    1.22 +by (fast_tac (!claset addIs prems) 1);
    1.23  qed "injI";
    1.24  
    1.25  val [major] = goal Fun.thy "(!!x. g(f(x)) = x) ==> inj(f)";
    1.26 @@ -109,7 +109,7 @@
    1.27  
    1.28  val prems = goalw Fun.thy [inj_onto_def]
    1.29      "(!! x y. [| f(x) = f(y);  x:A;  y:A |] ==> x=y) ==> inj_onto f A";
    1.30 -by (fast_tac (HOL_cs addIs prems addSIs [ballI]) 1);
    1.31 +by (fast_tac (!claset addIs prems addSIs [ballI]) 1);
    1.32  qed "inj_ontoI";
    1.33  
    1.34  val [major] = goal Fun.thy 
    1.35 @@ -126,7 +126,7 @@
    1.36  qed "inj_ontoD";
    1.37  
    1.38  goal Fun.thy "!!x y.[| inj_onto f A;  x:A;  y:A |] ==> (f(x)=f(y)) = (x=y)";
    1.39 -by (fast_tac (HOL_cs addSEs [inj_ontoD]) 1);
    1.40 +by (fast_tac (!claset addSEs [inj_ontoD]) 1);
    1.41  qed "inj_onto_iff";
    1.42  
    1.43  val major::prems = goal Fun.thy
    1.44 @@ -142,12 +142,12 @@
    1.45  val prems = goalw Fun.thy [o_def]
    1.46      "[| inj(f);  inj_onto g (range f) |] ==> inj(g o f)";
    1.47  by (cut_facts_tac prems 1);
    1.48 -by (fast_tac (HOL_cs addIs [injI,rangeI]
    1.49 +by (fast_tac (!claset addIs [injI,rangeI]
    1.50                       addEs [injD,inj_ontoD]) 1);
    1.51  qed "comp_inj";
    1.52  
    1.53  val [prem] = goal Fun.thy "inj(f) ==> inj_onto f A";
    1.54 -by (fast_tac (HOL_cs addIs [prem RS injD, inj_ontoI]) 1);
    1.55 +by (fast_tac (!claset addIs [prem RS injD, inj_ontoI]) 1);
    1.56  qed "inj_imp";
    1.57  
    1.58  val [prem] = goalw Fun.thy [Inv_def] "y : range(f) ==> f(Inv f y) = y";
    1.59 @@ -163,19 +163,28 @@
    1.60  val prems = goal Fun.thy
    1.61      "[| inj(f);  A<=range(f) |] ==> inj_onto (Inv f) A";
    1.62  by (cut_facts_tac prems 1);
    1.63 -by (fast_tac (HOL_cs addIs [inj_ontoI] 
    1.64 +by (fast_tac (!claset addIs [inj_ontoI] 
    1.65                       addEs [Inv_injective,injD,subsetD]) 1);
    1.66  qed "inj_onto_Inv";
    1.67  
    1.68  
    1.69  (*** Set reasoning tools ***)
    1.70  
    1.71 +AddSIs [ballI, PowI, subsetI, InterI, INT_I, INT1_I, CollectI, 
    1.72 +            ComplI, IntI, DiffI, UnCI, insertCI]; 
    1.73 +AddIs  [bexI, UnionI, UN_I, UN1_I, imageI, rangeI]; 
    1.74 +AddSEs [bexE, make_elim PowD, UnionE, UN_E, UN1_E, DiffE,
    1.75 +	    make_elim singleton_inject,
    1.76 +            CollectE, ComplE, IntE, UnE, insertE, imageE, rangeE, emptyE]; 
    1.77 +AddEs  [ballE, InterD, InterE, INT_D, INT_E, make_elim INT1_D,
    1.78 +            subsetD, subsetCE];
    1.79 +
    1.80  val set_cs = HOL_cs 
    1.81      addSIs [ballI, PowI, subsetI, InterI, INT_I, INT1_I, CollectI, 
    1.82              ComplI, IntI, DiffI, UnCI, insertCI] 
    1.83      addIs  [bexI, UnionI, UN_I, UN1_I, imageI, rangeI] 
    1.84      addSEs [bexE, make_elim PowD, UnionE, UN_E, UN1_E, DiffE,
    1.85 -	    make_elim singleton_inject,
    1.86 +            make_elim singleton_inject,
    1.87              CollectE, ComplE, IntE, UnE, insertE, imageE, rangeE, emptyE] 
    1.88      addEs  [ballE, InterD, InterE, INT_D, INT_E, make_elim INT1_D,
    1.89              subsetD, subsetCE];