src/HOL/Fun.ML
changeset 4089 96fba19bcbe2
parent 4059 59c1422c9da5
child 4656 134d24ddaad3
     1.1 --- a/src/HOL/Fun.ML	Mon Nov 03 12:12:10 1997 +0100
     1.2 +++ b/src/HOL/Fun.ML	Mon Nov 03 12:13:18 1997 +0100
     1.3 @@ -23,7 +23,7 @@
     1.4  
     1.5  val prems = goalw Fun.thy [inj_def]
     1.6      "[| !! x y. f(x) = f(y) ==> x=y |] ==> inj(f)";
     1.7 -by (blast_tac (!claset addIs prems) 1);
     1.8 +by (blast_tac (claset() addIs prems) 1);
     1.9  qed "injI";
    1.10  
    1.11  val [major] = goal Fun.thy "(!!x. g(f(x)) = x) ==> inj(f)";
    1.12 @@ -69,7 +69,7 @@
    1.13  
    1.14  val prems = goalw Fun.thy [inj_onto_def]
    1.15      "(!! x y. [| f(x) = f(y);  x:A;  y:A |] ==> x=y) ==> inj_onto f A";
    1.16 -by (blast_tac (!claset addIs prems) 1);
    1.17 +by (blast_tac (claset() addIs prems) 1);
    1.18  qed "inj_ontoI";
    1.19  
    1.20  val [major] = goal Fun.thy 
    1.21 @@ -86,7 +86,7 @@
    1.22  qed "inj_ontoD";
    1.23  
    1.24  goal Fun.thy "!!x y.[| inj_onto f A;  x:A;  y:A |] ==> (f(x)=f(y)) = (x=y)";
    1.25 -by (blast_tac (!claset addSDs [inj_ontoD]) 1);
    1.26 +by (blast_tac (claset() addSDs [inj_ontoD]) 1);
    1.27  qed "inj_onto_iff";
    1.28  
    1.29  val major::prems = goal Fun.thy
    1.30 @@ -106,11 +106,11 @@
    1.31  
    1.32  goalw Fun.thy [o_def]
    1.33      "!!f g. [| inj(f);  inj_onto g (range f) |] ==> inj(g o f)";
    1.34 -by (fast_tac (!claset addIs [injI] addEs [injD, inj_ontoD]) 1);
    1.35 +by (fast_tac (claset() addIs [injI] addEs [injD, inj_ontoD]) 1);
    1.36  qed "comp_inj";
    1.37  
    1.38  val [prem] = goal Fun.thy "inj(f) ==> inj_onto f A";
    1.39 -by (blast_tac (!claset addIs [prem RS injD, inj_ontoI]) 1);
    1.40 +by (blast_tac (claset() addIs [prem RS injD, inj_ontoI]) 1);
    1.41  qed "inj_imp";
    1.42  
    1.43  val [prem] = goalw Fun.thy [inv_def] "y : range(f) ==> f(inv f y) = y";
    1.44 @@ -124,7 +124,7 @@
    1.45  qed "inv_injective";
    1.46  
    1.47  goal Fun.thy "!!f. [| inj(f);  A<=range(f) |] ==> inj_onto (inv f) A";
    1.48 -by (fast_tac (!claset addIs [inj_ontoI] 
    1.49 +by (fast_tac (claset() addIs [inj_ontoI] 
    1.50                        addEs [inv_injective,injD]) 1);
    1.51  qed "inj_onto_inv";
    1.52  
    1.53 @@ -147,4 +147,4 @@
    1.54  qed "image_set_diff";
    1.55  
    1.56  
    1.57 -val set_cs = !claset delrules [equalityI];
    1.58 +val set_cs = claset() delrules [equalityI];