# HG changeset patch
# User berghofe
# Date 832855026 -7200
# Node ID 6f41a494f3b153190999435febb947ef2264de34
# Parent  a42d6c537f4a9d36d8d51d5f80cc99837bd580e7
Replaced fast_tac by Fast_tac (which uses default claset)
New rules are now also added to default claset.

diff -r a42d6c537f4a -r 6f41a494f3b1 src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Wed May 22 18:32:37 1996 +0200
+++ b/src/HOL/Arith.ML	Thu May 23 14:37:06 1996 +0200
@@ -47,7 +47,7 @@
 by (etac rev_mp 1);
 by (nat_ind_tac "k" 1);
 by (Simp_tac 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 val lemma = result();
 
 (* [| 0 < k; !!j. [| j: nat; k = succ(j) |] ==> Q |] ==> Q *)
@@ -233,7 +233,7 @@
 (*In ordinary notation: if 0<n and n<=m then m-n < m *)
 goal Arith.thy "!!m. [| 0<n; ~ m<n |] ==> m - n < m";
 by (subgoal_tac "0<n --> ~ m<n --> m - n < m" 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
 by (ALLGOALS(asm_simp_tac(!simpset addsimps [diff_less_Suc])));
 qed "diff_less";
@@ -321,7 +321,7 @@
 
 goal Arith.thy "P(k) --> (!n. P(Suc(n))--> P(n)) --> P(k-i)";
 by (res_inst_tac [("m","k"),("n","i")] diff_induct 1);
-by (ALLGOALS (strip_tac THEN' Simp_tac THEN' TRY o fast_tac HOL_cs));
+by (ALLGOALS (strip_tac THEN' Simp_tac THEN' TRY o Fast_tac));
 qed "zero_induct_lemma";
 
 val prems = goal Arith.thy "[| P(k);  !!n. P(Suc(n)) ==> P(n) |] ==> P(0)";
@@ -366,11 +366,13 @@
 
 val less_cs = set_cs addSEs [less_zeroE, less_SucE];
 
+AddSEs [less_zeroE, less_SucE];
+
 goal thy "!!k b. b<2 ==> k mod 2 = b | k mod 2 = (if b=1 then 0 else 1)";
 by (subgoal_tac "k mod 2 < 2" 1);
 by (asm_simp_tac (!simpset addsimps [mod_less_divisor]) 2);
 by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
-by (fast_tac less_cs 1);
+by (Fast_tac 1);
 qed "mod2_cases";
 
 goal thy "Suc(Suc(m)) mod 2 = m mod 2";
@@ -434,7 +436,7 @@
 by (etac rev_mp 1);
 by (nat_ind_tac "j" 1);
 by (ALLGOALS Asm_simp_tac);
-by (fast_tac (HOL_cs addDs [Suc_lessD]) 1);
+by (fast_tac (!claset addDs [Suc_lessD]) 1);
 qed "add_lessD1";
 
 goal Arith.thy "!!k::nat. m <= n ==> m <= n+k";
@@ -450,7 +452,7 @@
 goal Arith.thy "m+k<=n --> m<=(n::nat)";
 by (nat_ind_tac "k" 1);
 by (ALLGOALS Asm_simp_tac);
-by (fast_tac (HOL_cs addDs [Suc_leD]) 1);
+by (fast_tac (!claset addDs [Suc_leD]) 1);
 qed_spec_mp "add_leD1";
 
 goal Arith.thy "!!k l::nat. [| k<l; m+l = k+n |] ==> m<n";
@@ -486,7 +488,7 @@
 \     |] ==> f(i) <= (f(j)::nat)";
 by (cut_facts_tac [le] 1);
 by (asm_full_simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1);
-by (fast_tac (HOL_cs addSIs [lt_mono]) 1);
+by (fast_tac (!claset addSIs [lt_mono]) 1);
 qed "less_mono_imp_le_mono";
 
 (*non-strict, in 1st argument*)
diff -r a42d6c537f4a -r 6f41a494f3b1 src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Wed May 22 18:32:37 1996 +0200
+++ b/src/HOL/Finite.ML	Thu May 23 14:37:06 1996 +0200
@@ -16,7 +16,7 @@
 qed "Fin_mono";
 
 goalw Finite.thy Fin.defs "Fin(A) <= Pow(A)";
-by (fast_tac (set_cs addSIs [lfp_lowerbound]) 1);
+by (fast_tac (!claset addSIs [lfp_lowerbound]) 1);
 qed "Fin_subset_Pow";
 
 (* A : Fin(B) ==> A <= B *)
@@ -55,7 +55,7 @@
 qed "Fin_subset";
 
 goal Finite.thy "(F Un G : Fin(A)) = (F: Fin(A) & G: Fin(A))";
-by (fast_tac (set_cs addIs [Fin_UnI] addDs
+by (fast_tac (!claset addIs [Fin_UnI] addDs
                 [Un_upper1 RS Fin_subset, Un_upper2 RS Fin_subset]) 1);
 qed "subset_Fin";
 Addsimps[subset_Fin];
@@ -63,7 +63,7 @@
 goal Finite.thy "(insert a A : Fin M) = (a:M & A : Fin M)";
 by (stac insert_is_Un 1);
 by (Simp_tac 1);
-by (fast_tac (set_cs addSIs Fin.intrs addDs [FinD]) 1);
+by (fast_tac (!claset addSIs Fin.intrs addDs [FinD]) 1);
 qed "insert_Fin";
 Addsimps[insert_Fin];
 
@@ -163,7 +163,7 @@
 section "Finite cardinality -- 'card'";
 
 goal Set.thy "{f i |i. P i | i=n} = insert (f n) {f i|i. P i}";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 val Collect_conv_insert = result();
 
 goalw Finite.thy [card_def] "card {} = 0";
@@ -197,7 +197,7 @@
 by (case_tac "? a. a:A" 1);
  by (res_inst_tac [("x","0")] exI 2);
  by (Simp_tac 2);
- by (fast_tac eq_cs 2);
+ by (Fast_tac 2);
 by (etac exE 1);
 by (simp_tac (!simpset addsimps [less_Suc_eq]) 1);
 by (rtac exI 1);
@@ -212,7 +212,7 @@
   by (res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
   by (SELECT_GOAL(safe_tac eq_cs)1);
    by (subgoal_tac "x ~= f m" 1);
-    by (fast_tac set_cs 2);
+    by (Fast_tac 2);
    by (subgoal_tac "? k. f k = x & k<m" 1);
     by (best_tac set_cs 2);
    by (SELECT_GOAL(safe_tac HOL_cs)1);
@@ -226,7 +226,7 @@
  by (res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
  by (SELECT_GOAL(safe_tac eq_cs)1);
   by (subgoal_tac "x ~= f m" 1);
-   by (fast_tac set_cs 2);
+   by (Fast_tac 2);
   by (subgoal_tac "? k. f k = x & k<m" 1);
    by (best_tac set_cs 2);
   by (SELECT_GOAL(safe_tac HOL_cs)1);
@@ -237,7 +237,7 @@
 by (res_inst_tac [("x","%j. if f j = f i then f m else f j")] exI 1);
 by (SELECT_GOAL(safe_tac eq_cs)1);
  by (subgoal_tac "x ~= f i" 1);
-  by (fast_tac set_cs 2);
+  by (Fast_tac 2);
  by (case_tac "x = f m" 1);
   by (res_inst_tac [("x","i")] exI 1);
   by (Asm_simp_tac 1);
@@ -305,8 +305,8 @@
 by (Asm_simp_tac 1);
 by (rtac card_insert_disjoint 1);
 by (rtac (major RSN (2,finite_subset)) 1);
-by (fast_tac set_cs 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
+by (Fast_tac 1);
 by (asm_simp_tac (!simpset addsimps [major RS card_insert_disjoint]) 1);
 qed "card_insert";
 Addsimps [card_insert];
diff -r a42d6c537f4a -r 6f41a494f3b1 src/HOL/Lfp.ML
--- a/src/HOL/Lfp.ML	Wed May 22 18:32:37 1996 +0200
+++ b/src/HOL/Lfp.ML	Thu May 23 14:37:06 1996 +0200
@@ -60,7 +60,7 @@
 goal Lfp.thy "!!f. [| mono f; f A <= A |] ==> lfp(f) <= A";
 by (rtac subsetI 1);
 by (EVERY[etac induct 1, atac 1, etac subsetD 1, rtac subsetD 1,
-                atac 2, fast_tac (set_cs addSEs [monoD]) 1]);
+                atac 2, fast_tac (!claset addSEs [monoD]) 1]);
 qed "Park_induct";
 
 (** Definition forms of lfp_Tarski and induct, to control unfolding **)
diff -r a42d6c537f4a -r 6f41a494f3b1 src/HOL/List.ML
--- a/src/HOL/List.ML	Wed May 22 18:32:37 1996 +0200
+++ b/src/HOL/List.ML	Thu May 23 14:37:06 1996 +0200
@@ -95,7 +95,7 @@
 goal List.thy "(Alls x:xs.P(x)) = (!x. x mem xs --> P(x))";
 by (list.induct_tac "xs" 1);
 by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 qed "list_all_mem_conv";
 
 
@@ -106,13 +106,13 @@
 \                         (!y ys. xs=y#ys --> P(f y ys)))";
 by (list.induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 qed "expand_list_case";
 
 goal List.thy  "(xs=[] --> P([])) & (!y ys. xs=y#ys --> P(y#ys)) --> P(xs)";
 by (list.induct_tac "xs" 1);
-by (fast_tac HOL_cs 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
+by (Fast_tac 1);
 bind_thm("list_eq_cases",
   impI RSN (2,allI RSN (2,allI RSN (2,impI RS (conjI RS (result() RS mp))))));
 
diff -r a42d6c537f4a -r 6f41a494f3b1 src/HOL/Nat.ML
--- a/src/HOL/Nat.ML	Wed May 22 18:32:37 1996 +0200
+++ b/src/HOL/Nat.ML	Thu May 23 14:37:06 1996 +0200
@@ -32,7 +32,7 @@
     "[| i: Nat;  P(Zero_Rep);   \
 \       !!j. [| j: Nat; P(j) |] ==> P(Suc_Rep(j)) |]  ==> P(i)";
 by (rtac ([Nat_def, Nat_fun_mono, major] MRS def_induct) 1);
-by (fast_tac (set_cs addIs prems) 1);
+by (fast_tac (!claset addIs prems) 1);
 qed "Nat_induct";
 
 val prems = goalw Nat.thy [Zero_def,Suc_def]
@@ -66,10 +66,10 @@
 val prems = goal Nat.thy 
     "[| n=0 ==> P;  !!x. n = Suc(x) ==> P |] ==> P";
 by (subgoal_tac "n=0 | (EX x. n = Suc(x))" 1);
-by (fast_tac (HOL_cs addSEs prems) 1);
+by (fast_tac (!claset addSEs prems) 1);
 by (nat_ind_tac "n" 1);
 by (rtac (refl RS disjI1) 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 qed "natE";
 
 (*** Isomorphisms: Abs_Nat and Rep_Nat ***)
@@ -128,18 +128,18 @@
 (*** nat_case -- the selection operator for nat ***)
 
 goalw Nat.thy [nat_case_def] "nat_case a f 0 = a";
-by (fast_tac (set_cs addIs [select_equality] addEs [Zero_neq_Suc]) 1);
+by (fast_tac (!claset addIs [select_equality] addEs [Zero_neq_Suc]) 1);
 qed "nat_case_0";
 
 goalw Nat.thy [nat_case_def] "nat_case a f (Suc k) = f(k)";
-by (fast_tac (set_cs addIs [select_equality] 
+by (fast_tac (!claset addIs [select_equality] 
                        addEs [make_elim Suc_inject, Suc_neq_Zero]) 1);
 qed "nat_case_Suc";
 
 (** Introduction rules for 'pred_nat' **)
 
 goalw Nat.thy [pred_nat_def] "(n, Suc(n)) : pred_nat";
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed "pred_natI";
 
 val major::prems = goalw Nat.thy [pred_nat_def]
@@ -152,9 +152,9 @@
 goalw Nat.thy [wf_def] "wf(pred_nat)";
 by (strip_tac 1);
 by (nat_ind_tac "x" 1);
-by (fast_tac (HOL_cs addSEs [mp, pred_natE, Pair_inject, 
+by (fast_tac (!claset addSEs [mp, pred_natE, Pair_inject, 
                              make_elim Suc_inject]) 2);
-by (fast_tac (HOL_cs addSEs [mp, pred_natE, Pair_inject, Zero_neq_Suc]) 1);
+by (fast_tac (!claset addSEs [mp, pred_natE, Pair_inject, Zero_neq_Suc]) 1);
 qed "wf_pred_nat";
 
 
@@ -231,7 +231,7 @@
 (** Elimination properties **)
 
 val prems = goalw Nat.thy [less_def] "n<m ==> ~ m<(n::nat)";
-by (fast_tac (HOL_cs addIs ([wf_pred_nat, wf_trancl RS wf_asym]@prems))1);
+by (fast_tac (!claset addIs ([wf_pred_nat, wf_trancl RS wf_asym]@prems))1);
 qed "less_not_sym";
 
 (* [| n(m; m(n |] ==> R *)
@@ -246,7 +246,7 @@
 bind_thm ("less_irrefl", (less_not_refl RS notE));
 
 goal Nat.thy "!!m. n<m ==> m ~= (n::nat)";
-by (fast_tac (HOL_cs addEs [less_irrefl]) 1);
+by (fast_tac (!claset addEs [less_irrefl]) 1);
 qed "less_not_refl2";
 
 
@@ -274,13 +274,13 @@
     "[| m < Suc(n);  m<n ==> P;  m=n ==> P |] ==> P";
 by (rtac (major RS lessE) 1);
 by (rtac eq 1);
-by (fast_tac (HOL_cs addSDs [Suc_inject]) 1);
+by (fast_tac (!claset addSDs [Suc_inject]) 1);
 by (rtac less 1);
-by (fast_tac (HOL_cs addSDs [Suc_inject]) 1);
+by (fast_tac (!claset addSDs [Suc_inject]) 1);
 qed "less_SucE";
 
 goal Nat.thy "(m < Suc(n)) = (m < n | m = n)";
-by (fast_tac (HOL_cs addSIs [lessI]
+by (fast_tac (!claset addSIs [lessI]
                      addEs  [less_trans, less_SucE]) 1);
 qed "less_Suc_eq";
 
@@ -306,7 +306,7 @@
 by (nat_ind_tac "n" 1);
 by (rtac impI 1);
 by (etac less_zeroE 1);
-by (fast_tac (HOL_cs addSIs [lessI RS less_SucI]
+by (fast_tac (!claset addSIs [lessI RS less_SucI]
                      addSDs [Suc_inject]
                      addEs  [less_trans, lessE]) 1);
 qed "Suc_lessD";
@@ -328,11 +328,11 @@
 
 val prems = goal Nat.thy "m<n ==> Suc(m) < Suc(n)";
 by (subgoal_tac "m<n --> Suc(m) < Suc(n)" 1);
-by (fast_tac (HOL_cs addIs prems) 1);
+by (fast_tac (!claset addIs prems) 1);
 by (nat_ind_tac "n" 1);
 by (rtac impI 1);
 by (etac less_zeroE 1);
-by (fast_tac (HOL_cs addSIs [lessI]
+by (fast_tac (!claset addSIs [lessI]
                      addSDs [Suc_inject]
                      addEs  [less_trans, lessE]) 1);
 qed "Suc_mono";
@@ -353,7 +353,7 @@
 Addsimps [Suc_less_eq];
 
 goal Nat.thy "~(Suc(n) < n)";
-by (fast_tac (HOL_cs addEs [Suc_lessD RS less_irrefl]) 1);
+by (fast_tac (!claset addEs [Suc_lessD RS less_irrefl]) 1);
 qed "not_Suc_n_less_n";
 Addsimps [not_Suc_n_less_n];
 
@@ -361,7 +361,7 @@
 by (nat_ind_tac "k" 1);
 by (ALLGOALS (asm_simp_tac (!simpset)));
 by (asm_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
-by (fast_tac (HOL_cs addDs [Suc_lessD]) 1);
+by (fast_tac (!claset addDs [Suc_lessD]) 1);
 qed_spec_mp "less_trans_Suc";
 
 (*"Less than" is a linear ordering*)
@@ -370,7 +370,7 @@
 by (nat_ind_tac "n" 1);
 by (rtac (refl RS disjI1 RS disjI2) 1);
 by (rtac (zero_less_Suc RS disjI1) 1);
-by (fast_tac (HOL_cs addIs [lessI, Suc_mono, less_SucI] addEs [lessE]) 1);
+by (fast_tac (!claset addIs [lessI, Suc_mono, less_SucI] addEs [lessE]) 1);
 qed "less_linear";
 
 qed_goal "nat_less_cases" Nat.thy 
@@ -439,40 +439,40 @@
 val leE = make_elim leD;
 
 goal Nat.thy "(~n<m) = (m<=(n::nat))";
-by (fast_tac (HOL_cs addIs [leI] addEs [leE]) 1);
+by (fast_tac (!claset addIs [leI] addEs [leE]) 1);
 qed "not_less_iff_le";
 
 goalw Nat.thy [le_def] "!!m. ~ m <= n ==> n<(m::nat)";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 qed "not_leE";
 
 goalw Nat.thy [le_def] "!!m. m < n ==> Suc(m) <= n";
 by (simp_tac (!simpset addsimps [less_Suc_eq]) 1);
-by (fast_tac (HOL_cs addEs [less_irrefl,less_asym]) 1);
+by (fast_tac (!claset addEs [less_irrefl,less_asym]) 1);
 qed "lessD";
 
 goalw Nat.thy [le_def] "!!m. Suc(m) <= n ==> m <= n";
 by (asm_full_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 qed "Suc_leD";
 
 goalw Nat.thy [le_def] "!!m. m <= n ==> m <= Suc n";
-by (fast_tac (HOL_cs addDs [Suc_lessD]) 1);
+by (fast_tac (!claset addDs [Suc_lessD]) 1);
 qed "le_SucI";
 Addsimps[le_SucI];
 
 goalw Nat.thy [le_def] "!!m. m < n ==> m <= (n::nat)";
-by (fast_tac (HOL_cs addEs [less_asym]) 1);
+by (fast_tac (!claset addEs [less_asym]) 1);
 qed "less_imp_le";
 
 goalw Nat.thy [le_def] "!!m. m <= n ==> m < n | m=(n::nat)";
 by (cut_facts_tac [less_linear] 1);
-by (fast_tac (HOL_cs addEs [less_irrefl,less_asym]) 1);
+by (fast_tac (!claset addEs [less_irrefl,less_asym]) 1);
 qed "le_imp_less_or_eq";
 
 goalw Nat.thy [le_def] "!!m. m<n | m=n ==> m <=(n::nat)";
 by (cut_facts_tac [less_linear] 1);
-by (fast_tac (HOL_cs addEs [less_irrefl,less_asym]) 1);
+by (fast_tac (!claset addEs [less_irrefl,less_asym]) 1);
 by (flexflex_tac);
 qed "less_or_eq_imp_le";
 
@@ -486,22 +486,22 @@
 
 val prems = goal Nat.thy "!!i. [| i <= j; j < k |] ==> i < (k::nat)";
 by (dtac le_imp_less_or_eq 1);
-by (fast_tac (HOL_cs addIs [less_trans]) 1);
+by (fast_tac (!claset addIs [less_trans]) 1);
 qed "le_less_trans";
 
 goal Nat.thy "!!i. [| i < j; j <= k |] ==> i < (k::nat)";
 by (dtac le_imp_less_or_eq 1);
-by (fast_tac (HOL_cs addIs [less_trans]) 1);
+by (fast_tac (!claset addIs [less_trans]) 1);
 qed "less_le_trans";
 
 goal Nat.thy "!!i. [| i <= j; j <= k |] ==> i <= (k::nat)";
 by (EVERY1[dtac le_imp_less_or_eq, dtac le_imp_less_or_eq,
-          rtac less_or_eq_imp_le, fast_tac (HOL_cs addIs [less_trans])]);
+          rtac less_or_eq_imp_le, fast_tac (!claset addIs [less_trans])]);
 qed "le_trans";
 
 val prems = goal Nat.thy "!!m. [| m <= n; n <= m |] ==> m = (n::nat)";
 by (EVERY1[dtac le_imp_less_or_eq, dtac le_imp_less_or_eq,
-          fast_tac (HOL_cs addEs [less_irrefl,less_asym])]);
+          fast_tac (!claset addEs [less_irrefl,less_asym])]);
 qed "le_anti_sym";
 
 goal Nat.thy "(Suc(n) <= Suc(m)) = (n <= m)";
@@ -516,9 +516,9 @@
 val [prem1,prem2] = goalw Nat.thy [Least_def]
     "[| P(k);  !!x. x<k ==> ~P(x) |] ==> (LEAST x.P(x)) = k";
 by (rtac select_equality 1);
-by (fast_tac (HOL_cs addSIs [prem1,prem2]) 1);
+by (fast_tac (!claset addSIs [prem1,prem2]) 1);
 by (cut_facts_tac [less_linear] 1);
-by (fast_tac (HOL_cs addSIs [prem1] addSDs [prem2]) 1);
+by (fast_tac (!claset addSIs [prem1] addSDs [prem2]) 1);
 qed "Least_equality";
 
 val [prem] = goal Nat.thy "P(k) ==> P(LEAST x.P(x))";
@@ -529,7 +529,7 @@
 by (res_inst_tac [("s","n")] (Least_equality RS ssubst) 1);
 by (assume_tac 1);
 by (assume_tac 2);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 qed "LeastI";
 
 (*Proof is almost identical to the one above!*)
@@ -541,7 +541,7 @@
 by (res_inst_tac [("s","n")] (Least_equality RS ssubst) 1);
 by (assume_tac 1);
 by (rtac le_refl 2);
-by (fast_tac (HOL_cs addIs [less_imp_le,le_trans]) 1);
+by (fast_tac (!claset addIs [less_imp_le,le_trans]) 1);
 qed "Least_le";
 
 val [prem] = goal Nat.thy "k < (LEAST x.P(x)) ==> ~P(k)";
@@ -558,19 +558,19 @@
 	fold_goals_tac [Least_def],
 	safe_tac (HOL_cs addSEs [LeastI]),
 	res_inst_tac [("n","j")] natE 1,
-	fast_tac HOL_cs 1,
-	fast_tac (HOL_cs addDs [Suc_less_SucD] addDs [not_less_Least]) 1,	
+	Fast_tac 1,
+	fast_tac (!claset addDs [Suc_less_SucD] addDs [not_less_Least]) 1,	
 	res_inst_tac [("n","k")] natE 1,
-	fast_tac HOL_cs 1,
+	Fast_tac 1,
 	hyp_subst_tac 1,
 	rewtac Least_def,
 	rtac (select_equality RS arg_cong RS sym) 1,
 	safe_tac HOL_cs,
 	dtac Suc_mono 1,
-	fast_tac HOL_cs 1,
+	Fast_tac 1,
 	cut_facts_tac [less_linear] 1,
 	safe_tac HOL_cs,
 	atac 2,
-	fast_tac HOL_cs 2,
+	Fast_tac 2,
 	dtac Suc_mono 1,
-	fast_tac HOL_cs 1]);
+	Fast_tac 1]);
diff -r a42d6c537f4a -r 6f41a494f3b1 src/HOL/RelPow.ML
--- a/src/HOL/RelPow.ML	Wed May 22 18:32:37 1996 +0200
+++ b/src/HOL/RelPow.ML	Thu May 23 14:37:06 1996 +0200
@@ -20,15 +20,15 @@
 
 goal RelPow.thy "!!R. [| (x,y) : R^n; (y,z):R |] ==> (x,z):R^(Suc n)";
 by (simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
-by (fast_tac comp_cs 1);
+by (Fast_tac 1);
 qed "rel_pow_Suc_I";
 
 goal RelPow.thy "!z. (x,y) : R --> (y,z):R^n -->  (x,z):R^(Suc n)";
 by (nat_ind_tac "n" 1);
 by (simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
-by (fast_tac comp_cs 1);
+by (Fast_tac 1);
 by (asm_full_simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
-by (fast_tac comp_cs 1);
+by (Fast_tac 1);
 qed_spec_mp "rel_pow_Suc_I2";
 
 goal RelPow.thy "!!R. [| (x,y) : R^0; x=y ==> P |] ==> P";
@@ -39,7 +39,7 @@
   "[| (x,z) : R^(Suc n);  !!y. [| (x,y) : R^n; (y,z) : R |] ==> P |] ==> P";
 by (cut_facts_tac [major] 1);
 by (asm_full_simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
-by (fast_tac (comp_cs addIs [minor]) 1);
+by (fast_tac (!claset addIs [minor]) 1);
 qed "rel_pow_Suc_E";
 
 val [p1,p2,p3] = goal RelPow.thy
@@ -57,8 +57,8 @@
 
 goal RelPow.thy "!x z. (x,z):R^(Suc n) --> (? y. (x,y):R & (y,z):R^n)";
 by (nat_ind_tac "n" 1);
-by (fast_tac (HOL_cs addIs [rel_pow_0_I] addEs [rel_pow_0_E,rel_pow_Suc_E]) 1);
-by (fast_tac (HOL_cs addIs [rel_pow_Suc_I] addEs[rel_pow_0_E,rel_pow_Suc_E]) 1);
+by (fast_tac (!claset addIs [rel_pow_0_I] addEs [rel_pow_0_E,rel_pow_Suc_E]) 1);
+by (fast_tac (!claset addIs [rel_pow_Suc_I] addEs[rel_pow_0_E,rel_pow_Suc_E]) 1);
 qed_spec_mp "rel_pow_Suc_D2";
 
 val [p1,p2,p3] = goal RelPow.thy
@@ -80,13 +80,13 @@
 goal RelPow.thy "!!p. p:R^* ==> p : (UN n. R^n)";
 by (split_all_tac 1);
 by (etac rtrancl_induct 1);
-by (ALLGOALS (fast_tac (rel_cs addIs [rel_pow_0_I,rel_pow_Suc_I])));
+by (ALLGOALS (fast_tac (!claset addIs [rel_pow_0_I,rel_pow_Suc_I])));
 qed "rtrancl_imp_UN_rel_pow";
 
 goal RelPow.thy "!y. (x,y):R^n --> (x,y):R^*";
 by (nat_ind_tac "n" 1);
-by (fast_tac (HOL_cs addIs [rtrancl_refl] addEs [rel_pow_0_E]) 1);
-by (fast_tac (trancl_cs addEs [rel_pow_Suc_E,rtrancl_into_rtrancl]) 1);
+by (fast_tac (!claset addIs [rtrancl_refl] addEs [rel_pow_0_E]) 1);
+by (fast_tac (!claset addEs [rel_pow_Suc_E,rtrancl_into_rtrancl]) 1);
 val lemma = result() RS spec RS mp;
 
 goal RelPow.thy "!!p. p:R^n ==> p:R^*";
@@ -95,5 +95,5 @@
 qed "rel_pow_imp_rtrancl";
 
 goal RelPow.thy "R^* = (UN n. R^n)";
-by (fast_tac (eq_cs addIs [rtrancl_imp_UN_rel_pow,rel_pow_imp_rtrancl]) 1);
+by (fast_tac (!claset addIs [rtrancl_imp_UN_rel_pow,rel_pow_imp_rtrancl]) 1);
 qed "rtrancl_is_UN_rel_pow";
diff -r a42d6c537f4a -r 6f41a494f3b1 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Wed May 22 18:32:37 1996 +0200
+++ b/src/HOL/Set.ML	Thu May 23 14:37:06 1996 +0200
@@ -188,7 +188,7 @@
 val ComplE = make_elim ComplD;
 
 qed_goal "Compl_iff" Set.thy "(c : Compl(A)) = (c~:A)"
- (fn _ => [ (fast_tac (HOL_cs addSIs [ComplI] addSEs [ComplE]) 1) ]);
+ (fn _ => [ (fast_tac (!claset addSIs [ComplI] addSEs [ComplE]) 1) ]);
 
 
 section "Binary union -- Un";
@@ -215,7 +215,7 @@
 qed "UnE";
 
 qed_goal "Un_iff" Set.thy "(c : A Un B) = (c:A | c:B)"
- (fn _ => [ (fast_tac (HOL_cs addSIs [UnCI] addSEs [UnE]) 1) ]);
+ (fn _ => [ (fast_tac (!claset addSIs [UnCI] addSEs [UnE]) 1) ]);
 
 
 section "Binary intersection -- Int";
@@ -241,7 +241,7 @@
 qed "IntE";
 
 qed_goal "Int_iff" Set.thy "(c : A Int B) = (c:A & c:B)"
- (fn _ => [ (fast_tac (HOL_cs addSIs [IntI] addSEs [IntE]) 1) ]);
+ (fn _ => [ (fast_tac (!claset addSIs [IntI] addSEs [IntE]) 1) ]);
 
 
 section "Set difference";
@@ -266,7 +266,7 @@
     (REPEAT (ares_tac (prems RL [DiffD1, DiffD2 RS notI]) 1)) ]);
 
 qed_goal "Diff_iff" Set.thy "(c : A-B) = (c:A & c~:B)"
- (fn _ => [ (fast_tac (HOL_cs addSIs [DiffI] addSEs [DiffE]) 1) ]);
+ (fn _ => [ (fast_tac (!claset addSIs [DiffI] addSEs [DiffE]) 1) ]);
 
 section "The empty set -- {}";
 
@@ -286,7 +286,7 @@
   [ (rtac (minor RS (major RS equalityD1 RS subsetD RS emptyE)) 1) ]);
 
 qed_goal "empty_iff" Set.thy "(c : {}) = False"
- (fn _ => [ (fast_tac (HOL_cs addSEs [emptyE]) 1) ]);
+ (fn _ => [ (fast_tac (!claset addSEs [emptyE]) 1) ]);
 
 
 section "Augmenting a set -- insert";
@@ -304,7 +304,7 @@
     (REPEAT (eresolve_tac (prems @ [CollectE]) 1)) ]);
 
 qed_goal "insert_iff" Set.thy "a : insert b A = (a=b | a:A)"
- (fn _ => [fast_tac (HOL_cs addIs [insertI1,insertI2] addSEs [insertE]) 1]);
+ (fn _ => [fast_tac (!claset addIs [insertI1,insertI2] addSEs [insertE]) 1]);
 
 (*Classical introduction rule*)
 qed_goal "insertCI" Set.thy "(a~:B ==> a=b) ==> a: insert b B"
@@ -323,7 +323,7 @@
     (REPEAT (eresolve_tac (prems @ [emptyE]) 1)) ]);
 
 goalw Set.thy [insert_def] "!!a. b : {a} ==> b=a";
-by (fast_tac (HOL_cs addSEs [emptyE,CollectE,UnE]) 1);
+by (fast_tac (!claset addSEs [emptyE,CollectE,UnE]) 1);
 qed "singletonD";
 
 val singletonE = make_elim singletonD;
diff -r a42d6c537f4a -r 6f41a494f3b1 src/HOL/Sexp.ML
--- a/src/HOL/Sexp.ML	Wed May 22 18:32:37 1996 +0200
+++ b/src/HOL/Sexp.ML	Thu May 23 14:37:06 1996 +0200
@@ -16,19 +16,24 @@
                    Numb_neq_Scons, Numb_neq_Leaf,
                    Scons_neq_Leaf, Scons_neq_Numb];
 
+AddSDs [Leaf_inject, Numb_inject, Scons_inject];
+AddSEs [Leaf_neq_Scons, Leaf_neq_Numb,
+                   Numb_neq_Scons, Numb_neq_Leaf,
+                   Scons_neq_Leaf, Scons_neq_Numb];
+
 goalw Sexp.thy [sexp_case_def] "sexp_case c d e (Leaf a) = c(a)";
 by (resolve_tac [select_equality] 1);
-by (ALLGOALS (fast_tac sexp_free_cs));
+by (ALLGOALS (Fast_tac));
 qed "sexp_case_Leaf";
 
 goalw Sexp.thy [sexp_case_def] "sexp_case c d e (Numb k) = d(k)";
 by (resolve_tac [select_equality] 1);
-by (ALLGOALS (fast_tac sexp_free_cs));
+by (ALLGOALS (Fast_tac));
 qed "sexp_case_Numb";
 
 goalw Sexp.thy [sexp_case_def] "sexp_case c d e (M$N) = e M N";
 by (resolve_tac [select_equality] 1);
-by (ALLGOALS (fast_tac sexp_free_cs));
+by (ALLGOALS (Fast_tac));
 qed "sexp_case_Scons";
 
 
@@ -46,21 +51,23 @@
 
 val sexp_cs = set_cs addIs sexp.intrs@[SigmaI, uprodI];
 
+AddIs (sexp.intrs@[SigmaI, uprodI]);
+
 goal Sexp.thy "range(Leaf) <= sexp";
-by (fast_tac sexp_cs 1);
+by (Fast_tac 1);
 qed "range_Leaf_subset_sexp";
 
 val [major] = goal Sexp.thy "M$N : sexp ==> M: sexp & N: sexp";
 by (rtac (major RS setup_induction) 1);
 by (etac sexp.induct 1);
 by (ALLGOALS 
-    (fast_tac (set_cs addSEs [Scons_neq_Leaf,Scons_neq_Numb,Scons_inject])));
+    (fast_tac (!claset addSEs [Scons_neq_Leaf,Scons_neq_Numb,Scons_inject])));
 qed "Scons_D";
 
 (** Introduction rules for 'pred_sexp' **)
 
 goalw Sexp.thy [pred_sexp_def] "pred_sexp <= sexp Times sexp";
-by (fast_tac sexp_cs 1);
+by (Fast_tac 1);
 qed "pred_sexp_subset_Sigma";
 
 (* (a,b) : pred_sexp^+ ==> a : sexp *)
@@ -71,12 +78,12 @@
 
 val prems = goalw Sexp.thy [pred_sexp_def]
     "[| M: sexp;  N: sexp |] ==> (M, M$N) : pred_sexp";
-by (fast_tac (set_cs addIs prems) 1);
+by (fast_tac (!claset addIs prems) 1);
 qed "pred_sexpI1";
 
 val prems = goalw Sexp.thy [pred_sexp_def]
     "[| M: sexp;  N: sexp |] ==> (N, M$N) : pred_sexp";
-by (fast_tac (set_cs addIs prems) 1);
+by (fast_tac (!claset addIs prems) 1);
 qed "pred_sexpI2";
 
 (*Combinations involving transitivity and the rules above*)
@@ -102,9 +109,9 @@
 goal Sexp.thy "wf(pred_sexp)";
 by (rtac (pred_sexp_subset_Sigma RS wfI) 1);
 by (etac sexp.induct 1);
-by (fast_tac (HOL_cs addSEs [mp, pred_sexpE, Pair_inject, Scons_inject]) 3);
-by (fast_tac (HOL_cs addSEs [mp, pred_sexpE, Pair_inject, Numb_neq_Scons]) 2);
-by (fast_tac (HOL_cs addSEs [mp, pred_sexpE, Pair_inject, Leaf_neq_Scons]) 1);
+by (fast_tac (!claset addSEs [mp, pred_sexpE, Pair_inject, Scons_inject]) 3);
+by (fast_tac (!claset addSEs [mp, pred_sexpE, Pair_inject, Numb_neq_Scons]) 2);
+by (fast_tac (!claset addSEs [mp, pred_sexpE, Pair_inject, Leaf_neq_Scons]) 1);
 qed "wf_pred_sexp";
 
 (*** sexp_rec -- by wf recursion on pred_sexp ***)
diff -r a42d6c537f4a -r 6f41a494f3b1 src/HOL/Sum.ML
--- a/src/HOL/Sum.ML	Wed May 22 18:32:37 1996 +0200
+++ b/src/HOL/Sum.ML	Thu May 23 14:37:06 1996 +0200
@@ -56,12 +56,12 @@
 
 val [major] = goalw Sum.thy [Inl_Rep_def] "Inl_Rep(a) = Inl_Rep(c) ==> a=c";
 by (rtac (major RS fun_cong RS fun_cong RS fun_cong RS iffE) 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 qed "Inl_Rep_inject";
 
 val [major] = goalw Sum.thy [Inr_Rep_def] "Inr_Rep(b) = Inr_Rep(d) ==> b=d";
 by (rtac (major RS fun_cong RS fun_cong RS fun_cong RS iffE) 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 qed "Inr_Rep_inject";
 
 goalw Sum.thy [Inl_def] "inj(Inl)";
@@ -81,11 +81,11 @@
 val Inr_inject = inj_Inr RS injD;
 
 goal Sum.thy "(Inl(x)=Inl(y)) = (x=y)";
-by (fast_tac (HOL_cs addSEs [Inl_inject]) 1);
+by (fast_tac (!claset addSEs [Inl_inject]) 1);
 qed "Inl_eq";
 
 goal Sum.thy "(Inr(x)=Inr(y)) = (x=y)";
-by (fast_tac (HOL_cs addSEs [Inr_inject]) 1);
+by (fast_tac (!claset addSEs [Inr_inject]) 1);
 qed "Inr_eq";
 
 (*** Rules for the disjoint sum of two SETS ***)
@@ -117,15 +117,19 @@
                     addSEs [plusE, Inl_neq_Inr, Inr_neq_Inl]
                     addSDs [Inl_inject, Inr_inject];
 
+AddSIs [InlI, InrI]; 
+AddSEs [plusE, Inl_neq_Inr, Inr_neq_Inl];
+AddSDs [Inl_inject, Inr_inject];
+
 
 (** sum_case -- the selection operator for sums **)
 
 goalw Sum.thy [sum_case_def] "sum_case f g (Inl x) = f(x)";
-by (fast_tac (sum_cs addIs [select_equality]) 1);
+by (fast_tac (!claset addIs [select_equality]) 1);
 qed "sum_case_Inl";
 
 goalw Sum.thy [sum_case_def] "sum_case f g (Inr x) = g(x)";
-by (fast_tac (sum_cs addIs [select_equality]) 1);
+by (fast_tac (!claset addIs [select_equality]) 1);
 qed "sum_case_Inr";
 
 (** Exhaustion rule for sums -- a degenerate form of induction **)
@@ -151,10 +155,10 @@
 by (rtac sumE 1);
 by (etac ssubst 1);
 by (stac sum_case_Inl 1);
-by (fast_tac (set_cs addSEs [make_elim Inl_inject, Inl_neq_Inr]) 1);
+by (fast_tac (!claset addSEs [make_elim Inl_inject, Inl_neq_Inr]) 1);
 by (etac ssubst 1);
 by (stac sum_case_Inr 1);
-by (fast_tac (set_cs addSEs [make_elim Inr_inject, Inr_neq_Inl]) 1);
+by (fast_tac (!claset addSEs [make_elim Inr_inject, Inr_neq_Inl]) 1);
 qed "expand_sum_case";
 
 Addsimps [Inl_eq, Inr_eq, Inl_Inr_eq, Inr_Inl_eq,  sum_case_Inl, sum_case_Inr];
@@ -171,7 +175,7 @@
 
 goalw Sum.thy [Part_def]
     "!!a b A h. [| a : A;  a=h(b) |] ==> a : Part A h";
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed "Part_eqI";
 
 val PartI = refl RSN (2,Part_eqI);
@@ -190,7 +194,7 @@
 qed "Part_subset";
 
 goal Sum.thy "!!A B. A<=B ==> Part A h <= Part B h";
-by (fast_tac (set_cs addSIs [PartI] addSEs [PartE]) 1);
+by (fast_tac (!claset addSIs [PartI] addSEs [PartE]) 1);
 qed "Part_mono";
 
 val basic_monos = basic_monos @ [Part_mono];
@@ -200,14 +204,14 @@
 qed "PartD1";
 
 goal Sum.thy "Part A (%x.x) = A";
-by (fast_tac (set_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
+by (fast_tac (!claset addIs [PartI,equalityI] addSEs [PartE]) 1);
 qed "Part_id";
 
 goal Sum.thy "Part (A Int B) h = (Part A h) Int (Part B h)";
-by (fast_tac (set_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
+by (fast_tac (!claset addIs [PartI,equalityI] addSEs [PartE]) 1);
 qed "Part_Int";
 
 (*For inductive definitions*)
 goal Sum.thy "Part (A Int {x.P x}) h = (Part A h) Int {x.P x}";
-by (fast_tac (set_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
+by (fast_tac (!claset addIs [PartI,equalityI] addSEs [PartE]) 1);
 qed "Part_Collect";
diff -r a42d6c537f4a -r 6f41a494f3b1 src/HOL/Trancl.ML
--- a/src/HOL/Trancl.ML	Wed May 22 18:32:37 1996 +0200
+++ b/src/HOL/Trancl.ML	Thu May 23 14:37:06 1996 +0200
@@ -20,14 +20,14 @@
 (*Reflexivity of rtrancl*)
 goal Trancl.thy "(a,a) : r^*";
 by (stac rtrancl_unfold 1);
-by (fast_tac rel_cs 1);
+by (Fast_tac 1);
 qed "rtrancl_refl";
 
 (*Closure under composition with r*)
 val prems = goal Trancl.thy
     "[| (a,b) : r^*;  (b,c) : r |] ==> (a,c) : r^*";
 by (stac rtrancl_unfold 1);
-by (fast_tac (rel_cs addIs prems) 1);
+by (fast_tac (!claset addIs prems) 1);
 qed "rtrancl_into_rtrancl";
 
 (*rtrancl of r contains r*)
@@ -49,7 +49,7 @@
 \     !!x y z.[| P((x,y)); (x,y): r^*; (y,z): r |]  ==>  P((x,z)) |] \
 \  ==>  P((a,b))";
 by (rtac ([rtrancl_def, rtrancl_fun_mono, major] MRS def_induct) 1);
-by (fast_tac (rel_cs addIs prems) 1);
+by (fast_tac (!claset addIs prems) 1);
 qed "rtrancl_full_induct";
 
 (*nice induction rule*)
@@ -61,11 +61,11 @@
 (*by induction on this formula*)
 by (subgoal_tac "! y. (a::'a,b) = (a,y) --> P(y)" 1);
 (*now solve first subgoal: this formula is sufficient*)
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 (*now do the induction*)
 by (resolve_tac [major RS rtrancl_full_induct] 1);
-by (fast_tac (rel_cs addIs prems) 1);
-by (fast_tac (rel_cs addIs prems) 1);
+by (fast_tac (!claset addIs prems) 1);
+by (fast_tac (!claset addIs prems) 1);
 qed "rtrancl_induct";
 
 bind_thm
@@ -77,7 +77,7 @@
 goalw Trancl.thy [trans_def] "trans(r^*)";
 by (safe_tac HOL_cs);
 by (eres_inst_tac [("b","z")] rtrancl_induct 1);
-by (ALLGOALS(fast_tac (HOL_cs addIs [rtrancl_into_rtrancl])));
+by (ALLGOALS(fast_tac (!claset addIs [rtrancl_into_rtrancl])));
 qed "trans_rtrancl";
 
 bind_thm ("rtrancl_trans", trans_rtrancl RS transD);
@@ -90,8 +90,8 @@
 \    |] ==> P";
 by (subgoal_tac "(a::'a) = b  | (? y. (a,y) : r^* & (y,b) : r)" 1);
 by (rtac (major RS rtrancl_induct) 2);
-by (fast_tac (set_cs addIs prems) 2);
-by (fast_tac (set_cs addIs prems) 2);
+by (fast_tac (!claset addIs prems) 2);
+by (fast_tac (!claset addIs prems) 2);
 by (REPEAT (eresolve_tac ([asm_rl,exE,disjE,conjE]@prems) 1));
 qed "rtranclE";
 
@@ -107,7 +107,7 @@
 by (rtac iffI 1);
 by (etac rtrancl_induct 1);
 by (rtac rtrancl_refl 1);
-by (fast_tac (HOL_cs addEs [rtrancl_trans]) 1);
+by (fast_tac (!claset addEs [rtrancl_trans]) 1);
 by (etac r_into_rtrancl 1);
 qed "rtrancl_idemp";
 Addsimps [rtrancl_idemp];
@@ -121,7 +121,7 @@
 by (dtac rtrancl_mono 1);
 by (dtac rtrancl_mono 1);
 by (Asm_full_simp_tac 1);
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "rtrancl_subset";
 
 goal Trancl.thy "!!R. (R^* Un S^*)^* = (R Un S)^*";
@@ -138,14 +138,14 @@
 by (rtac converseI 1);
 by (etac rtrancl_induct 1);
 by (rtac rtrancl_refl 1);
-by (fast_tac (rel_cs addIs [r_into_rtrancl,rtrancl_trans]) 1);
+by (fast_tac (!claset addIs [r_into_rtrancl,rtrancl_trans]) 1);
 qed "rtrancl_converseD";
 
 goal Trancl.thy "!!r. (x,y) : converse(r^*) ==> (x,y) : (converse r)^*";
 by (dtac converseD 1);
 by (etac rtrancl_induct 1);
 by (rtac rtrancl_refl 1);
-by (fast_tac (rel_cs addIs [r_into_rtrancl,rtrancl_trans]) 1);
+by (fast_tac (!claset addIs [r_into_rtrancl,rtrancl_trans]) 1);
 qed "rtrancl_converseI";
 
 goal Trancl.thy "(converse r)^* = converse(r^*)";
@@ -161,7 +161,7 @@
 \     ==> P(a)";
 br ((major RS converseI RS rtrancl_converseI) RS rtrancl_induct) 1;
  brs prems 1;
-by(fast_tac (HOL_cs addIs prems addSEs[converseD]addSDs[rtrancl_converseD])1);
+by(fast_tac (!claset addIs prems addSEs[converseD]addSDs[rtrancl_converseD])1);
 qed "converse_rtrancl_induct";
 
 val prems = goal Trancl.thy
@@ -221,9 +221,9 @@
 (*by induction on this formula*)
 by (subgoal_tac "ALL z. (y,z) : r --> P(z)" 1);
 (*now solve first subgoal: this formula is sufficient*)
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 by (etac rtrancl_induct 1);
-by (ALLGOALS (fast_tac (set_cs addIs (rtrancl_into_trancl1::prems))));
+by (ALLGOALS (fast_tac (!claset addIs (rtrancl_into_trancl1::prems))));
 qed "trancl_induct";
 
 (*elimination of r^+ -- NOT an induction rule*)
@@ -236,8 +236,8 @@
 by (REPEAT (eresolve_tac ([asm_rl,disjE,exE,conjE]@prems) 1));
 by (rtac (rewrite_rule [trancl_def] major RS compEpair) 1);
 by (etac rtranclE 1);
-by (fast_tac rel_cs 1);
-by (fast_tac (rel_cs addSIs [rtrancl_into_trancl1]) 1);
+by (Fast_tac 1);
+by (fast_tac (!claset addSIs [rtrancl_into_trancl1]) 1);
 qed "tranclE";
 
 (*Transitivity of r^+.
@@ -264,15 +264,15 @@
 by (cut_facts_tac prems 1);
 by (rtac (major RS rtrancl_induct) 1);
 by (rtac (refl RS disjI1) 1);
-by (fast_tac (rel_cs addSEs [SigmaE2]) 1);
+by (fast_tac (!claset addSEs [SigmaE2]) 1);
 val lemma = result();
 
 goalw Trancl.thy [trancl_def]
     "!!r. r <= A Times A ==> r^+ <= A Times A";
-by (fast_tac (rel_cs addSDs [lemma]) 1);
+by (fast_tac (!claset addSDs [lemma]) 1);
 qed "trancl_subset_Sigma";
 
 (* Don't add r_into_rtrancl: it messes up the proofs in Lambda *)
 val trancl_cs = rel_cs addIs [rtrancl_refl];
 
-
+AddIs [rtrancl_refl];
diff -r a42d6c537f4a -r 6f41a494f3b1 src/HOL/Univ.ML
--- a/src/HOL/Univ.ML	Wed May 22 18:32:37 1996 +0200
+++ b/src/HOL/Univ.ML	Thu May 23 14:37:06 1996 +0200
@@ -69,12 +69,12 @@
 (*** Introduction rules for Node ***)
 
 goalw Univ.thy [Node_def] "(%k. 0,a) : Node";
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed "Node_K0_I";
 
 goalw Univ.thy [Node_def,Push_def]
     "!!p. p: Node ==> apfst (Push i) p : Node";
-by (fast_tac (set_cs addSIs [apfst_conv, nat_case_Suc RS trans]) 1);
+by (fast_tac (!claset addSIs [apfst_conv, nat_case_Suc RS trans]) 1);
 qed "Node_Push_I";
 
 
@@ -100,7 +100,7 @@
 (** Atomic nodes **)
 
 goalw Univ.thy [Atom_def, inj_def] "inj(Atom)";
-by (fast_tac (prod_cs addSIs [Node_K0_I] addSDs [Abs_Node_inject]) 1);
+by (fast_tac (!claset addSIs [Node_K0_I] addSDs [Abs_Node_inject]) 1);
 qed "inj_Atom";
 val Atom_inject = inj_Atom RS injD;
 
@@ -139,13 +139,13 @@
 
 val [major] = goalw Univ.thy [Scons_def] "M$N <= M'$N' ==> M<=M'";
 by (cut_facts_tac [major] 1);
-by (fast_tac (set_cs addSDs [Suc_inject]
+by (fast_tac (!claset addSDs [Suc_inject]
                      addSEs [Push_Node_inject, Zero_neq_Suc]) 1);
 qed "Scons_inject_lemma1";
 
 val [major] = goalw Univ.thy [Scons_def] "M$N <= M'$N' ==> N<=N'";
 by (cut_facts_tac [major] 1);
-by (fast_tac (set_cs addSDs [Suc_inject]
+by (fast_tac (!claset addSDs [Suc_inject]
                      addSEs [Push_Node_inject, Suc_neq_Zero]) 1);
 qed "Scons_inject_lemma2";
 
@@ -167,11 +167,11 @@
 
 (*rewrite rules*)
 goal Univ.thy "(Atom(a)=Atom(b)) = (a=b)";
-by (fast_tac (HOL_cs addSEs [Atom_inject]) 1);
+by (fast_tac (!claset addSEs [Atom_inject]) 1);
 qed "Atom_Atom_eq";
 
 goal Univ.thy "(M$N = M'$N') = (M=M' & N=N')";
-by (fast_tac (HOL_cs addSEs [Scons_inject]) 1);
+by (fast_tac (!claset addSEs [Scons_inject]) 1);
 qed "Scons_Scons_eq";
 
 (*** Distinctness involving Leaf and Numb ***)
@@ -323,11 +323,11 @@
 (*** Disjoint Sum ***)
 
 goalw Univ.thy [usum_def] "!!M. M:A ==> In0(M) : A<+>B";
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed "usum_In0I";
 
 goalw Univ.thy [usum_def] "!!N. N:B ==> In1(N) : A<+>B";
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed "usum_In1I";
 
 val major::prems = goalw Univ.thy [usum_def]
@@ -364,12 +364,12 @@
 (*** proving equality of sets and functions using ntrunc ***)
 
 goalw Univ.thy [ntrunc_def] "ntrunc k M <= M";
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed "ntrunc_subsetI";
 
 val [major] = goalw Univ.thy [ntrunc_def]
     "(!!k. ntrunc k M <= N) ==> M<=N";
-by (fast_tac (set_cs addIs [less_add_Suc1, less_add_Suc2, 
+by (fast_tac (!claset addIs [less_add_Suc1, less_add_Suc2, 
                             major RS subsetD]) 1);
 qed "ntrunc_subsetD";
 
@@ -391,15 +391,15 @@
 (*** Monotonicity ***)
 
 goalw Univ.thy [uprod_def] "!!A B. [| A<=A';  B<=B' |] ==> A<*>B <= A'<*>B'";
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed "uprod_mono";
 
 goalw Univ.thy [usum_def] "!!A B. [| A<=A';  B<=B' |] ==> A<+>B <= A'<+>B'";
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed "usum_mono";
 
 goalw Univ.thy [Scons_def] "!!M N. [| M<=M';  N<=N' |] ==> M$N <= M'$N'";
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed "Scons_mono";
 
 goalw Univ.thy [In0_def] "!!M N. M<=N ==> In0(M) <= In0(N)";
@@ -414,31 +414,31 @@
 (*** Split and Case ***)
 
 goalw Univ.thy [Split_def] "Split c (M$N) = c M N";
-by (fast_tac (set_cs addIs [select_equality] addEs [Scons_inject]) 1);
+by (fast_tac (!claset addIs [select_equality] addEs [Scons_inject]) 1);
 qed "Split";
 
 goalw Univ.thy [Case_def] "Case c d (In0 M) = c(M)";
-by (fast_tac (set_cs addIs [select_equality] 
+by (fast_tac (!claset addIs [select_equality] 
                      addEs [make_elim In0_inject, In0_neq_In1]) 1);
 qed "Case_In0";
 
 goalw Univ.thy [Case_def] "Case c d (In1 N) = d(N)";
-by (fast_tac (set_cs addIs [select_equality] 
+by (fast_tac (!claset addIs [select_equality] 
                      addEs [make_elim In1_inject, In1_neq_In0]) 1);
 qed "Case_In1";
 
 (**** UN x. B(x) rules ****)
 
 goalw Univ.thy [ntrunc_def] "ntrunc k (UN x.f(x)) = (UN x. ntrunc k (f x))";
-by (fast_tac (set_cs addIs [equalityI]) 1);
+by (fast_tac (!claset addIs [equalityI]) 1);
 qed "ntrunc_UN1";
 
 goalw Univ.thy [Scons_def] "(UN x.f(x)) $ M = (UN x. f(x) $ M)";
-by (fast_tac (set_cs addIs [equalityI]) 1);
+by (fast_tac (!claset addIs [equalityI]) 1);
 qed "Scons_UN1_x";
 
 goalw Univ.thy [Scons_def] "M $ (UN x.f(x)) = (UN x. M $ f(x))";
-by (fast_tac (set_cs addIs [equalityI]) 1);
+by (fast_tac (!claset addIs [equalityI]) 1);
 qed "Scons_UN1_y";
 
 goalw Univ.thy [In0_def] "In0(UN x.f(x)) = (UN x. In0(f(x)))";
@@ -453,7 +453,7 @@
 (*** Equality : the diagonal relation ***)
 
 goalw Univ.thy [diag_def] "!!a A. [| a=b;  a:A |] ==> (a,b) : diag(A)";
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed "diag_eqI";
 
 val diagI = refl RS diag_eqI |> standard;
@@ -471,7 +471,7 @@
 
 goalw Univ.thy [dprod_def]
     "!!r s. [| (M,M'):r;  (N,N'):s |] ==> (M$N, M'$N') : r<**>s";
-by (fast_tac prod_cs 1);
+by (Fast_tac 1);
 qed "dprodI";
 
 (*The general elimination rule*)
@@ -488,11 +488,11 @@
 (*** Equality for Disjoint Sum ***)
 
 goalw Univ.thy [dsum_def]  "!!r. (M,M'):r ==> (In0(M), In0(M')) : r<++>s";
-by (fast_tac prod_cs 1);
+by (Fast_tac 1);
 qed "dsum_In0I";
 
 goalw Univ.thy [dsum_def]  "!!r. (N,N'):s ==> (In1(N), In1(N')) : r<++>s";
-by (fast_tac prod_cs 1);
+by (Fast_tac 1);
 qed "dsum_In1I";
 
 val major::prems = goalw Univ.thy [dsum_def]
@@ -511,26 +511,29 @@
             addIs  [usum_In0I, usum_In1I, dsum_In0I, dsum_In1I]
             addSEs [diagE, uprodE, dprodE, usumE, dsumE];
 
+AddSIs [diagI, uprodI, dprodI];
+AddIs  [usum_In0I, usum_In1I, dsum_In0I, dsum_In1I];
+AddSEs [diagE, uprodE, dprodE, usumE, dsumE];
 
 (*** Monotonicity ***)
 
 goal Univ.thy "!!r s. [| r<=r';  s<=s' |] ==> r<**>s <= r'<**>s'";
-by (fast_tac univ_cs 1);
+by (Fast_tac 1);
 qed "dprod_mono";
 
 goal Univ.thy "!!r s. [| r<=r';  s<=s' |] ==> r<++>s <= r'<++>s'";
-by (fast_tac univ_cs 1);
+by (Fast_tac 1);
 qed "dsum_mono";
 
 
 (*** Bounding theorems ***)
 
 goal Univ.thy "diag(A) <= A Times A";
-by (fast_tac univ_cs 1);
+by (Fast_tac 1);
 qed "diag_subset_Sigma";
 
 goal Univ.thy "((A Times B) <**> (C Times D)) <= (A<*>C) Times (B<*>D)";
-by (fast_tac univ_cs 1);
+by (Fast_tac 1);
 qed "dprod_Sigma";
 
 val dprod_subset_Sigma = [dprod_mono, dprod_Sigma] MRS subset_trans |>standard;
@@ -540,11 +543,11 @@
     "(Sigma A B <**> Sigma C D) <= Sigma (A<*>C) (Split(%x y. B(x)<*>D(y)))";
 by (safe_tac univ_cs);
 by (stac Split 1);
-by (fast_tac univ_cs 1);
+by (Fast_tac 1);
 qed "dprod_subset_Sigma2";
 
 goal Univ.thy "(A Times B <++> C Times D) <= (A<+>C) Times (B<+>D)";
-by (fast_tac univ_cs 1);
+by (Fast_tac 1);
 qed "dsum_Sigma";
 
 val dsum_subset_Sigma = [dsum_mono, dsum_Sigma] MRS subset_trans |> standard;
@@ -553,16 +556,16 @@
 (*** Domain ***)
 
 goal Univ.thy "fst `` diag(A) = A";
-by (fast_tac (prod_cs addIs [equalityI, diagI] addSEs [diagE]) 1);
+by (fast_tac (!claset addIs [equalityI, diagI] addSEs [diagE]) 1);
 qed "fst_image_diag";
 
 goal Univ.thy "fst `` (r<**>s) = (fst``r) <*> (fst``s)";
-by (fast_tac (prod_cs addIs [equalityI, uprodI, dprodI]
+by (fast_tac (!claset addIs [equalityI, uprodI, dprodI]
                      addSEs [uprodE, dprodE]) 1);
 qed "fst_image_dprod";
 
 goal Univ.thy "fst `` (r<++>s) = (fst``r) <+> (fst``s)";
-by (fast_tac (prod_cs addIs [equalityI, usum_In0I, usum_In1I, 
+by (fast_tac (!claset addIs [equalityI, usum_In0I, usum_In1I, 
                              dsum_In0I, dsum_In1I]
                      addSEs [usumE, dsumE]) 1);
 qed "fst_image_dsum";
diff -r a42d6c537f4a -r 6f41a494f3b1 src/HOL/WF.ML
--- a/src/HOL/WF.ML	Wed May 22 18:32:37 1996 +0200
+++ b/src/HOL/WF.ML	Thu May 23 14:37:06 1996 +0200
@@ -27,7 +27,7 @@
 \       !!x.[| ! y. (y,x): r --> P(y) |] ==> P(x) \
 \    |]  ==>  P(a)";
 by (rtac (major RS spec RS mp RS spec) 1);
-by (fast_tac (HOL_cs addEs prems) 1);
+by (fast_tac (!claset addEs prems) 1);
 qed "wf_induct";
 
 (*Perform induction on i, then prove the wf(r) subgoal using prems. *)
@@ -38,9 +38,9 @@
 
 val prems = goal WF.thy "[| wf(r);  (a,x):r;  (x,a):r |] ==> P";
 by (subgoal_tac "! x. (a,x):r --> (x,a):r --> P" 1);
-by (fast_tac (HOL_cs addIs prems) 1);
+by (fast_tac (!claset addIs prems) 1);
 by (wf_ind_tac "a" prems 1);
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed "wf_asym";
 
 val prems = goal WF.thy "[| wf(r);  (a,a): r |] ==> P";
@@ -58,8 +58,8 @@
 by (res_inst_tac [("a","x")] (prem RS wf_induct) 1);
 by (rtac (impI RS allI) 1);
 by (etac tranclE 1);
-by (fast_tac HOL_cs 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
+by (Fast_tac 1);
 qed "wf_trancl";
 
 
diff -r a42d6c537f4a -r 6f41a494f3b1 src/HOL/mono.ML
--- a/src/HOL/mono.ML	Wed May 22 18:32:37 1996 +0200
+++ b/src/HOL/mono.ML	Thu May 23 14:37:06 1996 +0200
@@ -7,58 +7,58 @@
 *)
 
 goal Set.thy "!!A B. A<=B ==> f``A <= f``B";
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed "image_mono";
 
 goal Set.thy "!!A B. A<=B ==> Pow(A) <= Pow(B)";
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed "Pow_mono";
 
 goal Set.thy "!!A B. A<=B ==> Union(A) <= Union(B)";
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed "Union_mono";
 
 goal Set.thy "!!A B. B<=A ==> Inter(A) <= Inter(B)";
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed "Inter_anti_mono";
 
 val prems = goal Set.thy
     "[| A<=B;  !!x. x:A ==> f(x)<=g(x) |] ==> \
 \    (UN x:A. f(x)) <= (UN x:B. g(x))";
-by (fast_tac (set_cs addIs (prems RL [subsetD])) 1);
+by (fast_tac (!claset addIs (prems RL [subsetD])) 1);
 qed "UN_mono";
 
 val [prem] = goal Set.thy
     "[| !!x. f(x)<=g(x) |] ==> (UN x. f(x)) <= (UN x. g(x))";
-by (fast_tac (set_cs addIs [prem RS subsetD]) 1);
+by (fast_tac (!claset addIs [prem RS subsetD]) 1);
 qed "UN1_mono";
 
 val prems = goal Set.thy
     "[| B<=A;  !!x. x:A ==> f(x)<=g(x) |] ==> \
 \    (INT x:A. f(x)) <= (INT x:A. g(x))";
-by (fast_tac (set_cs addIs (prems RL [subsetD])) 1);
+by (fast_tac (!claset addIs (prems RL [subsetD])) 1);
 qed "INT_anti_mono";
 
 (*The inclusion is POSITIVE! *)
 val [prem] = goal Set.thy
     "[| !!x. f(x)<=g(x) |] ==> (INT x. f(x)) <= (INT x. g(x))";
-by (fast_tac (set_cs addIs [prem RS subsetD]) 1);
+by (fast_tac (!claset addIs [prem RS subsetD]) 1);
 qed "INT1_mono";
 
 goal Set.thy "!!A B. [| A<=C;  B<=D |] ==> A Un B <= C Un D";
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed "Un_mono";
 
 goal Set.thy "!!A B. [| A<=C;  B<=D |] ==> A Int B <= C Int D";
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed "Int_mono";
 
 goal Set.thy "!!A::'a set. [| A<=C;  D<=B |] ==> A-B <= C-D";
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed "Diff_mono";
 
 goal Set.thy "!!A B. A<=B ==> Compl(B) <= Compl(A)";
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed "Compl_anti_mono";
 
 (** Monotonicity of implications.  For inductive definitions **)
@@ -70,15 +70,15 @@
 qed "in_mono";
 
 goal HOL.thy "!!P1 P2 Q1 Q2. [| P1-->Q1; P2-->Q2 |] ==> (P1&P2) --> (Q1&Q2)";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 qed "conj_mono";
 
 goal HOL.thy "!!P1 P2 Q1 Q2. [| P1-->Q1; P2-->Q2 |] ==> (P1|P2) --> (Q1|Q2)";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 qed "disj_mono";
 
 goal HOL.thy "!!P1 P2 Q1 Q2.[| Q1-->P1; P2-->Q2 |] ==> (P1-->P2)-->(Q1-->Q2)";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 qed "imp_mono";
 
 goal HOL.thy "P-->P";
@@ -88,24 +88,24 @@
 
 val [PQimp] = goal HOL.thy
     "[| !!x. P(x) --> Q(x) |] ==> (EX x.P(x)) --> (EX x.Q(x))";
-by (fast_tac (HOL_cs addIs [PQimp RS mp]) 1);
+by (fast_tac (!claset addIs [PQimp RS mp]) 1);
 qed "ex_mono";
 
 val [PQimp] = goal HOL.thy
     "[| !!x. P(x) --> Q(x) |] ==> (ALL x.P(x)) --> (ALL x.Q(x))";
-by (fast_tac (HOL_cs addIs [PQimp RS mp]) 1);
+by (fast_tac (!claset addIs [PQimp RS mp]) 1);
 qed "all_mono";
 
 val [PQimp] = goal Set.thy
     "[| !!x. P(x) --> Q(x) |] ==> Collect(P) <= Collect(Q)";
-by (fast_tac (set_cs addIs [PQimp RS mp]) 1);
+by (fast_tac (!claset addIs [PQimp RS mp]) 1);
 qed "Collect_mono";
 
 (*Used in indrule.ML*)
 val [subs,PQimp] = goal Set.thy
     "[| A<=B;  !!x. x:A ==> P(x) --> Q(x) \
 \    |] ==> A Int Collect(P) <= B Int Collect(Q)";
-by (fast_tac (set_cs addIs [subs RS subsetD, PQimp RS mp]) 1);
+by (fast_tac (!claset addIs [subs RS subsetD, PQimp RS mp]) 1);
 qed "Int_Collect_mono";
 
 (*Used in intr_elim.ML and in individual datatype definitions*)
diff -r a42d6c537f4a -r 6f41a494f3b1 src/HOL/subset.ML
--- a/src/HOL/subset.ML	Wed May 22 18:32:37 1996 +0200
+++ b/src/HOL/subset.ML	Thu May 23 14:37:06 1996 +0200
@@ -13,11 +13,11 @@
  (fn _=> [ (rtac subsetI 1), (etac insertI2 1) ]);
 
 goal Set.thy "!!x. x ~: A ==> (A <= insert x B) = (A <= B)";
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed "subset_insert";
 
 qed_goal "subset_empty_iff" Set.thy "(A<={}) = (A={})"
- (fn _=> [ (fast_tac (set_cs addIs [equalityI]) 1) ]);
+ (fn _=> [ (fast_tac (!claset addIs [equalityI]) 1) ]);
 
 (*** Big Union -- least upper bound of a set  ***)