reflecting my recent changes of the simplifier and classical reasoner
authoroheimb
Sat Feb 15 17:52:31 1997 +0100 (1997-02-15)
changeset 2637e9b203f854ae
parent 2636 4b30dbe4a020
child 2638 6c6a44b5f757
reflecting my recent changes of the simplifier and classical reasoner
src/HOL/Auth/Message.ML
src/HOL/Auth/NS_Public.ML
src/HOL/Auth/NS_Public_Bad.ML
src/HOL/Auth/NS_Shared.ML
src/HOL/Auth/OtwayRees.ML
src/HOL/Auth/OtwayRees_AN.ML
src/HOL/Auth/OtwayRees_Bad.ML
src/HOL/Auth/Public.ML
src/HOL/Auth/Recur.ML
src/HOL/Auth/Shared.ML
src/HOL/Auth/WooLam.ML
src/HOL/Auth/Yahalom.ML
src/HOL/Auth/Yahalom2.ML
src/HOL/IMP/Transition.ML
src/HOL/Lambda/Lambda.ML
src/HOL/Lambda/ParRed.ML
src/HOL/MiniML/W.ML
src/HOL/Prod.ML
src/HOL/Relation.ML
src/HOL/W0/I.ML
src/HOL/W0/Type.ML
src/HOL/W0/W.ML
src/HOL/WF.ML
src/HOL/ex/Comb.ML
src/HOL/indrule.ML
src/ZF/Arith.ML
src/ZF/Epsilon.ML
src/ZF/List.ML
src/ZF/Order.ML
src/ZF/Perm.ML
src/ZF/WF.ML
src/ZF/ex/Bin.ML
src/ZF/ex/Primrec.ML
src/ZF/ex/TF.ML
src/ZF/ex/Term.ML
src/ZF/indrule.ML
     1.1 --- a/src/HOL/Auth/Message.ML	Sat Feb 15 17:48:19 1997 +0100
     1.2 +++ b/src/HOL/Auth/Message.ML	Sat Feb 15 17:52:31 1997 +0100
     1.3 @@ -825,13 +825,6 @@
     1.4  (*Cannot be added with Addsimps -- we don't always want to re-order messages*)
     1.5  val pushes = pushKeys@pushCrypts;
     1.6  
     1.7 -
     1.8 -(*No premature instantiation of variables during simplification.
     1.9 -  For proving "possibility" properties.*)
    1.10 -fun safe_solver prems =
    1.11 -    match_tac (TrueI::refl::prems) ORELSE' eq_assume_tac
    1.12 -    ORELSE' etac FalseE;
    1.13 -
    1.14  val Fake_insert_tac = 
    1.15      dresolve_tac [impOfSubs Fake_analz_insert,
    1.16                    impOfSubs Fake_parts_insert] THEN'
     2.1 --- a/src/HOL/Auth/NS_Public.ML	Sat Feb 15 17:48:19 1997 +0100
     2.2 +++ b/src/HOL/Auth/NS_Public.ML	Sat Feb 15 17:52:31 1997 +0100
     2.3 @@ -12,6 +12,8 @@
     2.4  proof_timing:=true;
     2.5  HOL_quantifiers := false;
     2.6  
     2.7 +val op addss = op unsafe_addss;
     2.8 +
     2.9  AddIffs [Spy_in_lost];
    2.10  
    2.11  (*Replacing the variable by a constant improves search speed by 50%!*)
     3.1 --- a/src/HOL/Auth/NS_Public_Bad.ML	Sat Feb 15 17:48:19 1997 +0100
     3.2 +++ b/src/HOL/Auth/NS_Public_Bad.ML	Sat Feb 15 17:52:31 1997 +0100
     3.3 @@ -16,6 +16,8 @@
     3.4  proof_timing:=true;
     3.5  HOL_quantifiers := false;
     3.6  
     3.7 +val op addss = op unsafe_addss;
     3.8 +
     3.9  AddIffs [Spy_in_lost];
    3.10  
    3.11  (*Replacing the variable by a constant improves search speed by 50%!*)
     4.1 --- a/src/HOL/Auth/NS_Shared.ML	Sat Feb 15 17:48:19 1997 +0100
     4.2 +++ b/src/HOL/Auth/NS_Shared.ML	Sat Feb 15 17:52:31 1997 +0100
     4.3 @@ -113,7 +113,7 @@
     4.4        (!claset addIs [impOfSubs analz_subset_parts]
     4.5                 addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
     4.6                        impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
     4.7 -               addss (!simpset)) 1);
     4.8 +               unsafe_addss (!simpset)) 1);
     4.9  (*NS2, NS4, NS5*)
    4.10  by (REPEAT (fast_tac (!claset addSEs sees_Spy_partsEs addss (!simpset)) 1));
    4.11  qed_spec_mp "new_keys_not_used";
    4.12 @@ -167,7 +167,7 @@
    4.13  \            | X : analz (sees lost Spy evs)";
    4.14  by (case_tac "A : lost" 1);
    4.15  by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
    4.16 -                      addss (!simpset)) 1);
    4.17 +                      unsafe_addss (!simpset)) 1);
    4.18  by (forward_tac [Says_imp_sees_Spy RS parts.Inj] 1);
    4.19  by (fast_tac (!claset addEs  partsEs
    4.20                        addSDs [A_trusts_NS2, Says_Server_message_form]
     5.1 --- a/src/HOL/Auth/OtwayRees.ML	Sat Feb 15 17:48:19 1997 +0100
     5.2 +++ b/src/HOL/Auth/OtwayRees.ML	Sat Feb 15 17:52:31 1997 +0100
     5.3 @@ -92,9 +92,9 @@
     5.4               (*Fake message*)
     5.5               TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
     5.6                                             impOfSubs Fake_parts_insert]
     5.7 -                                    addss (!simpset)) 2)) THEN
     5.8 +                            unsafe_addss (!simpset)) 2)) THEN
     5.9       (*Base case*)
    5.10 -     fast_tac (!claset addss (!simpset)) 1 THEN
    5.11 +     fast_tac (!claset unsafe_addss (!simpset)) 1 THEN
    5.12       ALLGOALS Asm_simp_tac) i;
    5.13  
    5.14  (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
    5.15 @@ -134,7 +134,7 @@
    5.16        (!claset addIs [impOfSubs analz_subset_parts]
    5.17                 addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
    5.18                        impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
    5.19 -               addss (!simpset)) 1);
    5.20 +               unsafe_addss (!simpset)) 1);
    5.21  (*OR1-3*)
    5.22  by (REPEAT (fast_tac (!claset addss (!simpset)) 1));
    5.23  qed_spec_mp "new_keys_not_used";
     6.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Sat Feb 15 17:48:19 1997 +0100
     6.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Sat Feb 15 17:52:31 1997 +0100
     6.3 @@ -123,7 +123,7 @@
     6.4        (!claset addIs [impOfSubs analz_subset_parts]
     6.5                 addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
     6.6                        impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
     6.7 -               addss (!simpset)) 1);
     6.8 +               unsafe_addss (!simpset)) 1);
     6.9  (*OR3*)
    6.10  by (fast_tac (!claset addss (!simpset)) 1);
    6.11  qed_spec_mp "new_keys_not_used";
    6.12 @@ -297,7 +297,7 @@
    6.13                        addIs [impOfSubs analz_subset_parts]
    6.14                        addss (!simpset addsimps [parts_insert2])) 2);
    6.15  (*Oops*) 
    6.16 -by (best_tac (!claset addDs [unique_session_keys] addss (!simpset)) 3);
    6.17 +by (best_tac (!claset addDs [unique_session_keys] unsafe_addss (!simpset)) 3);
    6.18  (*OR4, Fake*) 
    6.19  by (REPEAT_FIRST spy_analz_tac);
    6.20  val lemma = result() RS mp RS mp RSN(2,rev_notE);
     7.1 --- a/src/HOL/Auth/OtwayRees_Bad.ML	Sat Feb 15 17:48:19 1997 +0100
     7.2 +++ b/src/HOL/Auth/OtwayRees_Bad.ML	Sat Feb 15 17:52:31 1997 +0100
     7.3 @@ -125,7 +125,7 @@
     7.4        (!claset addIs [impOfSubs analz_subset_parts]
     7.5                 addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
     7.6                        impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
     7.7 -               addss (!simpset)) 1);
     7.8 +               unsafe_addss (!simpset)) 1);
     7.9  (*OR1-3*)
    7.10  by (REPEAT (fast_tac (!claset addss (!simpset)) 1));
    7.11  qed_spec_mp "new_keys_not_used";
     8.1 --- a/src/HOL/Auth/Public.ML	Sat Feb 15 17:48:19 1997 +0100
     8.2 +++ b/src/HOL/Auth/Public.ML	Sat Feb 15 17:52:31 1997 +0100
     8.3 @@ -186,7 +186,7 @@
     8.4  by (fast_tac (!claset addSEs [add_leE]) 2);
     8.5  (*Nonce case*)
     8.6  by (res_inst_tac [("x","N + Suc nat")] exI 1);
     8.7 -by (fast_tac (!claset addSEs [add_leE] addafter (TRYALL trans_tac)) 1);
     8.8 +by (fast_tac (!claset addSEs [add_leE] addaltern trans_tac) 1);
     8.9  val lemma = result();
    8.10  
    8.11  goal thy "Nonce (@ N. Nonce N ~: used evs) ~: used evs";
    8.12 @@ -198,7 +198,7 @@
    8.13  (*Tactic for possibility theorems*)
    8.14  val possibility_tac =
    8.15      REPEAT 
    8.16 -    (ALLGOALS (simp_tac (!simpset setsolver safe_solver))
    8.17 +    (ALLGOALS (simp_tac (!simpset setSolver safe_solver))
    8.18       THEN
    8.19       REPEAT_FIRST (eq_assume_tac ORELSE' 
    8.20                     resolve_tac [refl, conjI, Nonce_supply]));
     9.1 --- a/src/HOL/Auth/Recur.ML	Sat Feb 15 17:48:19 1997 +0100
     9.2 +++ b/src/HOL/Auth/Recur.ML	Sat Feb 15 17:52:31 1997 +0100
     9.3 @@ -157,9 +157,9 @@
     9.4               (*Fake message*)
     9.5               TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
     9.6                                             impOfSubs Fake_parts_insert]
     9.7 -                                    addss (!simpset)) 2)) THEN
     9.8 +                            unsafe_addss (!simpset)) 2)) THEN
     9.9       (*Base case*)
    9.10 -     fast_tac (!claset addss (!simpset)) 1 THEN
    9.11 +     fast_tac (!claset unsafe_addss (!simpset)) 1 THEN
    9.12       ALLGOALS Asm_simp_tac) i;
    9.13  
    9.14  (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
    9.15 @@ -178,7 +178,7 @@
    9.16                        addss (!simpset addsimps [parts_insert_sees])) 2);
    9.17  (*RA2*)
    9.18  by (best_tac (!claset addSEs partsEs addSDs [parts_cut]
    9.19 -                      addss (!simpset)) 1);
    9.20 +                      unsafe_addss (!simpset)) 1);
    9.21  qed "Spy_see_shrK";
    9.22  Addsimps [Spy_see_shrK];
    9.23  
    9.24 @@ -215,13 +215,13 @@
    9.25  by (parts_induct_tac 1);
    9.26  (*RA3*)
    9.27  by (best_tac (!claset addDs  [Key_in_keysFor_parts]
    9.28 -                      addss  (!simpset addsimps [parts_insert_sees])) 2);
    9.29 +                      unsafe_addss  (!simpset addsimps [parts_insert_sees])) 2);
    9.30  (*Fake*)
    9.31  by (best_tac
    9.32        (!claset addIs [impOfSubs analz_subset_parts]
    9.33                 addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
    9.34                        impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
    9.35 -               addss (!simpset)) 1);
    9.36 +               unsafe_addss (!simpset)) 1);
    9.37  qed_spec_mp "new_keys_not_used";
    9.38  
    9.39  
    9.40 @@ -574,5 +574,5 @@
    9.41                        addSIs [disjI2]
    9.42                        addSEs [MPair_parts]
    9.43                        addDs  [parts.Body]
    9.44 -                      addss  (!simpset)) 0 1);
    9.45 +                      unsafe_addss  (!simpset)) 0 1);
    9.46  qed "Cert_imp_Server_msg";
    10.1 --- a/src/HOL/Auth/Shared.ML	Sat Feb 15 17:48:19 1997 +0100
    10.2 +++ b/src/HOL/Auth/Shared.ML	Sat Feb 15 17:52:31 1997 +0100
    10.3 @@ -140,7 +140,7 @@
    10.4  by (Step_tac 1);
    10.5  by (etac rev_mp 1);     (*split_tac does not work on assumptions*)
    10.6  by (ALLGOALS
    10.7 -    (fast_tac (!claset addss (!simpset addsimps [parts_Un, sees_Cons] 
    10.8 +    (fast_tac (!claset unsafe_addss (!simpset addsimps [parts_Un, sees_Cons] 
    10.9                         setloop split_tac [expand_if]))));
   10.10  qed "UN_parts_sees_Says";
   10.11  
   10.12 @@ -157,7 +157,7 @@
   10.13   "!!evs. [| Says A B (Crypt (shrK C) X) : set_of_list evs;  C : lost |] \
   10.14  \        ==> X : analz (sees lost Spy evs)";
   10.15  by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
   10.16 -                      addss (!simpset)) 1);
   10.17 +                      unsafe_addss (!simpset)) 1);
   10.18  qed "Says_Crypt_lost";
   10.19  
   10.20  goal thy  
   10.21 @@ -165,7 +165,7 @@
   10.22  \           X ~: analz (sees lost Spy evs) |]                     \
   10.23  \        ==> C ~: lost";
   10.24  by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
   10.25 -                      addss (!simpset)) 1);
   10.26 +                      unsafe_addss (!simpset)) 1);
   10.27  qed "Says_Crypt_not_lost";
   10.28  
   10.29  (*NEEDED??*)
   10.30 @@ -267,7 +267,7 @@
   10.31  by (fast_tac (!claset addSEs [add_leE]) 2);
   10.32  (*Nonce case*)
   10.33  by (res_inst_tac [("x","N + Suc nat")] exI 1);
   10.34 -by (fast_tac (!claset addSEs [add_leE] addafter (TRYALL trans_tac)) 1);
   10.35 +by (fast_tac (!claset addSEs [add_leE] addaltern trans_tac) 1);
   10.36  val lemma = result();
   10.37  
   10.38  goal thy "EX N. Nonce N ~: used evs";
   10.39 @@ -352,7 +352,7 @@
   10.40  val possibility_tac =
   10.41      REPEAT (*omit used_Says so that Nonces, Keys start from different traces!*)
   10.42      (ALLGOALS (simp_tac 
   10.43 -               (!simpset delsimps [used_Says] setsolver safe_solver))
   10.44 +               (!simpset delsimps [used_Says] setSolver safe_solver))
   10.45       THEN
   10.46       REPEAT_FIRST (eq_assume_tac ORELSE' 
   10.47                     resolve_tac [refl, conjI, Nonce_supply, Key_supply]));
   10.48 @@ -361,7 +361,7 @@
   10.49    nonces and keys initially*)
   10.50  val basic_possibility_tac =
   10.51      REPEAT 
   10.52 -    (ALLGOALS (asm_simp_tac (!simpset setsolver safe_solver))
   10.53 +    (ALLGOALS (asm_simp_tac (!simpset setSolver safe_solver))
   10.54       THEN
   10.55       REPEAT_FIRST (resolve_tac [refl, conjI]));
   10.56  
    11.1 --- a/src/HOL/Auth/WooLam.ML	Sat Feb 15 17:48:19 1997 +0100
    11.2 +++ b/src/HOL/Auth/WooLam.ML	Sat Feb 15 17:52:31 1997 +0100
    11.3 @@ -26,10 +26,10 @@
    11.4  by (REPEAT (resolve_tac [exI,bexI] 1));
    11.5  by (rtac (woolam.Nil RS woolam.WL1 RS woolam.WL2 RS woolam.WL3 RS 
    11.6            woolam.WL4 RS woolam.WL5) 2);
    11.7 -by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
    11.8 +by (ALLGOALS (simp_tac (!simpset setSolver safe_solver)));
    11.9  by (REPEAT_FIRST (resolve_tac [refl, conjI]));
   11.10  by (REPEAT_FIRST (fast_tac (!claset addSEs [Nonce_supply RS notE]
   11.11 -                                    addss (!simpset setsolver safe_solver))));
   11.12 +                                    addss (!simpset setSolver safe_solver))));
   11.13  result();
   11.14  
   11.15  
    12.1 --- a/src/HOL/Auth/Yahalom.ML	Sat Feb 15 17:48:19 1997 +0100
    12.2 +++ b/src/HOL/Auth/Yahalom.ML	Sat Feb 15 17:52:31 1997 +0100
    12.3 @@ -16,6 +16,8 @@
    12.4  HOL_quantifiers := false;
    12.5  Pretty.setdepth 25;
    12.6  
    12.7 +val op addss = op unsafe_addss;
    12.8 +
    12.9  
   12.10  (*A "possibility property": there are traces that reach the end*)
   12.11  goal thy 
    13.1 --- a/src/HOL/Auth/Yahalom2.ML	Sat Feb 15 17:48:19 1997 +0100
    13.2 +++ b/src/HOL/Auth/Yahalom2.ML	Sat Feb 15 17:52:31 1997 +0100
    13.3 @@ -17,6 +17,7 @@
    13.4  proof_timing:=true;
    13.5  HOL_quantifiers := false;
    13.6  
    13.7 +val op addss = op unsafe_addss;
    13.8  
    13.9  (*A "possibility property": there are traces that reach the end*)
   13.10  goal thy 
    14.1 --- a/src/HOL/IMP/Transition.ML	Sat Feb 15 17:48:19 1997 +0100
    14.2 +++ b/src/HOL/IMP/Transition.ML	Sat Feb 15 17:52:31 1997 +0100
    14.3 @@ -201,7 +201,7 @@
    14.4    "(c,s) -*-> (c',s') ==> <c',s'> -c-> t --> <c,s> -c-> t";
    14.5  by (rtac (major RS rtrancl_induct2) 1);
    14.6  by (Fast_tac 1);
    14.7 -by (fast_tac (!claset addIs [FB_lemma3] addbefore (split_all_tac 1)) 1);
    14.8 +by (fast_tac (!claset addIs [FB_lemma3] addbefore split_all_tac) 1);
    14.9  qed_spec_mp "FB_lemma2";
   14.10  
   14.11  goal Transition.thy "!!c. (c,s) -*-> (SKIP,t) ==> <c,s> -c-> t";
    15.1 --- a/src/HOL/Lambda/Lambda.ML	Sat Feb 15 17:48:19 1997 +0100
    15.2 +++ b/src/HOL/Lambda/Lambda.ML	Sat Feb 15 17:52:31 1997 +0100
    15.3 @@ -66,7 +66,7 @@
    15.4    "!i k. i < Suc k --> lift (lift t i) (Suc k) = lift (lift t k) i";
    15.5  by (dB.induct_tac "t" 1);
    15.6  by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])
    15.7 -                                    addsolver (cut_trans_tac))));
    15.8 +                                    addSolver cut_trans_tac)));
    15.9  by (safe_tac HOL_cs);
   15.10  by (ALLGOALS trans_tac);
   15.11  qed_spec_mp "lift_lift";
   15.12 @@ -76,7 +76,7 @@
   15.13  by (dB.induct_tac "t" 1);
   15.14  by (ALLGOALS(asm_simp_tac (!simpset addsimps [pred_def,subst_Var,lift_lift]
   15.15                                  setloop (split_tac [expand_if,expand_nat_case])
   15.16 -                                addsolver (cut_trans_tac))));
   15.17 +                                addSolver cut_trans_tac)));
   15.18  by (safe_tac HOL_cs);
   15.19  by (ALLGOALS trans_tac);
   15.20  qed "lift_subst";
   15.21 @@ -88,7 +88,7 @@
   15.22  by (dB.induct_tac "t" 1);
   15.23  by (ALLGOALS(asm_simp_tac (!simpset addsimps [subst_Var,lift_lift]
   15.24                                  setloop (split_tac [expand_if])
   15.25 -                                addsolver (cut_trans_tac))));
   15.26 +                                addSolver cut_trans_tac)));
   15.27  by(safe_tac (HOL_cs addSEs [nat_neqE]));
   15.28  by(ALLGOALS trans_tac);
   15.29  qed "lift_subst_lt";
   15.30 @@ -106,7 +106,7 @@
   15.31  by (ALLGOALS(asm_simp_tac
   15.32        (!simpset addsimps [pred_def,subst_Var,lift_lift RS sym,lift_subst_lt]
   15.33                  setloop (split_tac [expand_if,expand_nat_case])
   15.34 -                addsolver (cut_trans_tac))));
   15.35 +                addSolver cut_trans_tac)));
   15.36  by(safe_tac (HOL_cs addSEs [nat_neqE]));
   15.37  by(ALLGOALS trans_tac);
   15.38  qed_spec_mp "subst_subst";
    16.1 --- a/src/HOL/Lambda/ParRed.ML	Sat Feb 15 17:48:19 1997 +0100
    16.2 +++ b/src/HOL/Lambda/ParRed.ML	Sat Feb 15 17:52:31 1997 +0100
    16.3 @@ -83,7 +83,7 @@
    16.4    by (Simp_tac 1);
    16.5   by (etac rev_mp 1);
    16.6   by (dB.induct_tac "dB1" 1);
    16.7 - by (ALLGOALS(fast_tac (!claset addSIs [par_beta_subst] addss !simpset)));
    16.8 + by (ALLGOALS(fast_tac (!claset addSIs [par_beta_subst] unsafe_addss (!simpset))));
    16.9  qed_spec_mp "par_beta_cd";
   16.10  
   16.11  (*** Confluence (via cd) ***)
    17.1 --- a/src/HOL/MiniML/W.ML	Sat Feb 15 17:48:19 1997 +0100
    17.2 +++ b/src/HOL/MiniML/W.ML	Sat Feb 15 17:52:31 1997 +0100
    17.3 @@ -492,7 +492,7 @@
    17.4  by (eres_inst_tac [("x","(FVar n)#A")] allE 1);
    17.5  by (eres_inst_tac [("x","t2")] allE 1);
    17.6  by (eres_inst_tac [("x","Suc n")] allE 1);
    17.7 -by (best_tac (HOL_cs addSDs [mk_scheme_injective] addss (!simpset addcongs [conj_cong] 
    17.8 +by (best_tac (HOL_cs addSDs [mk_scheme_injective] unsafe_addss (!simpset addcongs [conj_cong] 
    17.9      setloop (split_tac [expand_option_bind]))) 1);
   17.10  
   17.11  (* case App e1 e2 *)
    18.1 --- a/src/HOL/Prod.ML	Sat Feb 15 17:48:19 1997 +0100
    18.2 +++ b/src/HOL/Prod.ML	Sat Feb 15 17:52:31 1997 +0100
    18.3 @@ -78,7 +78,7 @@
    18.4  end;
    18.5  
    18.6  goal Prod.thy "(!x. P x) = (!a b. P(a,b))";
    18.7 -by (fast_tac (!claset addbefore split_all_tac 1) 1);
    18.8 +by (fast_tac (!claset addbefore split_all_tac) 1);
    18.9  qed "split_paired_All";
   18.10  
   18.11  goalw Prod.thy [split_def] "split c (a,b) = c a b";
    19.1 --- a/src/HOL/Relation.ML	Sat Feb 15 17:48:19 1997 +0100
    19.2 +++ b/src/HOL/Relation.ML	Sat Feb 15 17:52:31 1997 +0100
    19.3 @@ -173,11 +173,11 @@
    19.4      (REPEAT (eresolve_tac [asm_rl, ImageE, subsetD RS SigmaD2] 1)) ]);
    19.5  
    19.6  goal Relation.thy "R O id = R";
    19.7 -by (fast_tac (!claset addbefore (split_all_tac 1)) 1);
    19.8 +by (fast_tac (!claset addbefore split_all_tac) 1);
    19.9  qed "R_O_id";
   19.10  
   19.11  goal Relation.thy "id O R = R";
   19.12 -by (fast_tac (!claset addbefore (split_all_tac 1)) 1);
   19.13 +by (fast_tac (!claset addbefore split_all_tac) 1);
   19.14  qed "id_O_R";
   19.15  
   19.16  Addsimps [R_O_id,id_O_R];
    20.1 --- a/src/HOL/W0/I.ML	Sat Feb 15 17:48:19 1997 +0100
    20.2 +++ b/src/HOL/W0/I.ML	Sat Feb 15 17:52:31 1997 +0100
    20.3 @@ -8,6 +8,8 @@
    20.4  
    20.5  open I;
    20.6  
    20.7 +val op addss = op unsafe_addss;
    20.8 +
    20.9  goal thy
   20.10    "! a m s s' t n.  \
   20.11  \    (new_tv m a & new_tv m s) --> I e a m s = Ok(s',t,n) -->   \
    21.1 --- a/src/HOL/W0/Type.ML	Sat Feb 15 17:48:19 1997 +0100
    21.2 +++ b/src/HOL/W0/Type.ML	Sat Feb 15 17:52:31 1997 +0100
    21.3 @@ -259,7 +259,7 @@
    21.4  (* case [] *)
    21.5  by (Simp_tac 1);
    21.6  (* case x#xl *)
    21.7 -by (fast_tac (set_cs addss (!simpset setloop (split_tac [expand_if]))) 1);
    21.8 +by (fast_tac (set_cs unsafe_addss(!simpset setloop (split_tac [expand_if]))) 1);
    21.9  qed_spec_mp "ftv_mem_sub_ftv_list";
   21.10  Addsimps [ftv_mem_sub_ftv_list];
   21.11  
    22.1 --- a/src/HOL/W0/W.ML	Sat Feb 15 17:48:19 1997 +0100
    22.2 +++ b/src/HOL/W0/W.ML	Sat Feb 15 17:52:31 1997 +0100
    22.3 @@ -45,7 +45,7 @@
    22.4          "!a n s t m. W e a n  = Ok (s,t,m) --> n<=m";
    22.5  by (expr.induct_tac "e" 1);
    22.6  (* case Var(n) *)
    22.7 -by (fast_tac (HOL_cs addss (!simpset setloop (split_tac [expand_if]))) 1);
    22.8 +by (fast_tac (HOL_cs unsafe_addss(!simpset setloop (split_tac [expand_if]))) 1);
    22.9  (* case Abs e *)
   22.10  by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
   22.11  by (fast_tac (HOL_cs addDs [Suc_leD]) 1);
   22.12 @@ -91,7 +91,7 @@
   22.13  \                 new_tv m s & new_tv m t";
   22.14  by (expr.induct_tac "e" 1);
   22.15  (* case Var n *)
   22.16 -by (fast_tac (HOL_cs addss (!simpset 
   22.17 +by (fast_tac (HOL_cs unsafe_addss (!simpset 
   22.18          addsimps [id_subst_def,list_all_nth,new_tv_list,new_tv_subst] 
   22.19          setloop (split_tac [expand_if]))) 1);
   22.20  
   22.21 @@ -161,7 +161,7 @@
   22.22  by (expr.induct_tac "e" 1);
   22.23  (* case Var n *)
   22.24  by (fast_tac (HOL_cs addIs [nth_mem,subsetD,ftv_mem_sub_ftv_list] 
   22.25 -    addss (!simpset setloop (split_tac [expand_if]))) 1);
   22.26 +    unsafe_addss (!simpset setloop (split_tac [expand_if]))) 1);
   22.27  
   22.28  (* case Abs e *)
   22.29  by (asm_full_simp_tac (!simpset addsimps
    23.1 --- a/src/HOL/WF.ML	Sat Feb 15 17:48:19 1997 +0100
    23.2 +++ b/src/HOL/WF.ML	Sat Feb 15 17:52:31 1997 +0100
    23.3 @@ -90,7 +90,7 @@
    23.4      (cut_facts_tac hyps THEN'
    23.5         DEPTH_SOLVE_1 o (ares_tac [TrueI] ORELSE'
    23.6                          eresolve_tac [transD, mp, allE]));
    23.7 -val wf_super_ss = HOL_ss addsolver indhyp_tac;
    23.8 +val wf_super_ss = HOL_ss addSolver indhyp_tac;
    23.9  
   23.10  val prems = goalw WF.thy [is_recfun_def,cut_def]
   23.11      "[| wf(r);  trans(r);  is_recfun r H a f;  is_recfun r H b g |] ==> \
    24.1 --- a/src/HOL/ex/Comb.ML	Sat Feb 15 17:48:19 1997 +0100
    24.2 +++ b/src/HOL/ex/Comb.ML	Sat Feb 15 17:52:31 1997 +0100
    24.3 @@ -55,7 +55,7 @@
    24.4  
    24.5  AddIs  contract.intrs;
    24.6  AddSEs [K_contractE, S_contractE, Ap_contractE];
    24.7 -Addss  (!simpset);
    24.8 +Unsafe_Addss  (!simpset);
    24.9  
   24.10  goalw Comb.thy [I_def] "!!z. I -1-> z ==> P";
   24.11  by (Fast_tac 1);
   24.12 @@ -106,7 +106,7 @@
   24.13  
   24.14  AddIs  parcontract.intrs;
   24.15  AddSEs [K_parcontractE, S_parcontractE,Ap_parcontractE];
   24.16 -Addss  (!simpset);
   24.17 +Unsafe_Addss  (!simpset);
   24.18  
   24.19  (*** Basic properties of parallel contraction ***)
   24.20  
    25.1 --- a/src/HOL/indrule.ML	Sat Feb 15 17:48:19 1997 +0100
    25.2 +++ b/src/HOL/indrule.ML	Sat Feb 15 17:52:31 1997 +0100
    25.3 @@ -85,10 +85,7 @@
    25.4    simplifications.  If the premises get simplified, then the proofs will 
    25.5    fail.  This arose with a premise of the form {(F n,G n)|n . True}, which
    25.6    expanded to something containing ...&True. *)
    25.7 -val min_ss = empty_ss
    25.8 -      setmksimps (mksimps mksimps_pairs)
    25.9 -      setsolver (fn prems => resolve_tac (TrueI::refl::prems) ORELSE' atac
   25.10 -                             ORELSE' etac FalseE);
   25.11 +val min_ss = HOL_basic_ss;
   25.12  
   25.13  val quant_induct = 
   25.14      prove_goalw_cterm part_rec_defs 
    26.1 --- a/src/ZF/Arith.ML	Sat Feb 15 17:48:19 1997 +0100
    26.2 +++ b/src/ZF/Arith.ML	Sat Feb 15 17:52:31 1997 +0100
    26.3 @@ -537,7 +537,7 @@
    26.4  qed "zero_lt_mult_iff";
    26.5  
    26.6  goal Arith.thy "!!k. [| m: nat; n: nat |] ==> m#*n = 1 <-> m=1 & n=1";
    26.7 -by (best_tac (!claset addEs [natE] addss (!simpset)) 1);
    26.8 +by (best_tac (!claset addEs [natE] unsafe_addss (!simpset)) 1);
    26.9  qed "mult_eq_1_iff";
   26.10  
   26.11  (*Cancellation law for division*)
   26.12 @@ -576,7 +576,7 @@
   26.13  by (rtac disjCI 1);
   26.14  by (dtac sym 1);
   26.15  by (rtac Ord_linear_lt 1 THEN REPEAT_SOME (ares_tac [nat_into_Ord,nat_1I]));
   26.16 -by (fast_tac (!claset addss (!simpset)) 1);
   26.17 +by (fast_tac (!claset unsafe_addss (!simpset)) 1);
   26.18  by (fast_tac (le_cs addDs [mono_lemma] 
   26.19                      addss (!simpset addsimps [mult_1_right])) 1);
   26.20  qed "mult_eq_self_implies_10";
    27.1 --- a/src/ZF/Epsilon.ML	Sat Feb 15 17:48:19 1997 +0100
    27.2 +++ b/src/ZF/Epsilon.ML	Sat Feb 15 17:52:31 1997 +0100
    27.3 @@ -313,7 +313,7 @@
    27.4  goal thy "transrec2(succ(i),a,b) = b(i, transrec2(i,a,b))";
    27.5  by (rtac (transrec2_def RS def_transrec RS trans) 1);
    27.6  by (simp_tac (!simpset addsimps [succ_not_0, THE_eq, if_P]
    27.7 -                    setsolver K Fast_tac) 1);
    27.8 +                    setSolver K Fast_tac) 1);
    27.9  qed "transrec2_succ";
   27.10  
   27.11  goal thy "!!i. Limit(i) ==> transrec2(i,a,b) = (UN j<i. transrec2(j,a,b))";
    28.1 --- a/src/ZF/List.ML	Sat Feb 15 17:48:19 1997 +0100
    28.2 +++ b/src/ZF/List.ML	Sat Feb 15 17:52:31 1997 +0100
    28.3 @@ -259,7 +259,7 @@
    28.4      [list_rec_type, map_type, map_type2, app_type, length_type, 
    28.5       rev_type, flat_type, list_add_type];
    28.6  
    28.7 -simpset := !simpset setsolver (type_auto_tac list_typechecks);
    28.8 +simpset := !simpset setSolver (type_auto_tac list_typechecks);
    28.9  
   28.10  
   28.11  (*** theorems about map ***)
    29.1 --- a/src/ZF/Order.ML	Sat Feb 15 17:48:19 1997 +0100
    29.2 +++ b/src/ZF/Order.ML	Sat Feb 15 17:52:31 1997 +0100
    29.3 @@ -11,6 +11,8 @@
    29.4  
    29.5  open Order;
    29.6  
    29.7 +val op addss = op unsafe_addss;
    29.8 +
    29.9  (** Basic properties of the definitions **)
   29.10  
   29.11  (*needed?*)
   29.12 @@ -237,11 +239,10 @@
   29.13  
   29.14  (*Rewriting with bijections and converse (function inverse)*)
   29.15  val bij_inverse_ss = 
   29.16 -    !simpset setsolver (type_auto_tac [ord_iso_is_bij, bij_is_fun, apply_type, 
   29.17 +    !simpset setSolver (type_auto_tac [ord_iso_is_bij, bij_is_fun, apply_type, 
   29.18                                         bij_converse_bij, comp_fun, comp_bij])
   29.19            addsimps [right_inverse_bij, left_inverse_bij];
   29.20  
   29.21 -
   29.22  (** Symmetry and Transitivity Rules **)
   29.23  
   29.24  (*Reflexivity of similarity*)
    30.1 --- a/src/ZF/Perm.ML	Sat Feb 15 17:48:19 1997 +0100
    30.2 +++ b/src/ZF/Perm.ML	Sat Feb 15 17:52:31 1997 +0100
    30.3 @@ -335,7 +335,7 @@
    30.4  by (rtac lam_funtype 2);
    30.5  by (typechk_tac (prem::ZF_typechecks));
    30.6  by (asm_simp_tac (!simpset 
    30.7 -             setsolver type_auto_tac [lam_type, lam_funtype, prem]) 1);
    30.8 +             setSolver type_auto_tac [lam_type, lam_funtype, prem]) 1);
    30.9  qed "comp_lam";
   30.10  
   30.11  goal Perm.thy "!!f g. [| g: inj(A,B);  f: inj(B,C) |] ==> (f O g) : inj(A,C)";
   30.12 @@ -343,7 +343,7 @@
   30.13      f_imp_injective 1);
   30.14  by (REPEAT (ares_tac [comp_fun, inj_is_fun] 1));
   30.15  by (asm_simp_tac (!simpset  addsimps [left_inverse] 
   30.16 -                        setsolver type_auto_tac [inj_is_fun, apply_type]) 1);
   30.17 +                        setSolver type_auto_tac [inj_is_fun, apply_type]) 1);
   30.18  qed "comp_inj";
   30.19  
   30.20  goalw Perm.thy [surj_def]
   30.21 @@ -544,7 +544,7 @@
   30.22      "!!f. [| f: inj(A,B);  a~:A;  b~:B |]  ==> \
   30.23  \         cons(<a,b>,f) : inj(cons(a,A), cons(b,B))";
   30.24  by (fast_tac (!claset  addIs [apply_type]
   30.25 -                     addss (!simpset addsimps [fun_extend, fun_extend_apply2,
   30.26 +              unsafe_addss (!simpset addsimps [fun_extend, fun_extend_apply2,
   30.27                                              fun_extend_apply1]) ) 1);
   30.28  qed "inj_extend";
   30.29  
    31.1 --- a/src/ZF/WF.ML	Sat Feb 15 17:48:19 1997 +0100
    31.2 +++ b/src/ZF/WF.ML	Sat Feb 15 17:52:31 1997 +0100
    31.3 @@ -225,7 +225,7 @@
    31.4                          eresolve_tac [underD, transD, spec RS mp]));
    31.5  
    31.6  (*** NOTE! some simplifications need a different solver!! ***)
    31.7 -val wf_super_ss = !simpset setsolver indhyp_tac;
    31.8 +val wf_super_ss = !simpset setSolver indhyp_tac;
    31.9  
   31.10  val prems = goalw WF.thy [is_recfun_def]
   31.11      "[| wf(r);  trans(r);  is_recfun(r,a,H,f);  is_recfun(r,b,H,g) |] ==> \
    32.1 --- a/src/ZF/ex/Bin.ML	Sat Feb 15 17:48:19 1997 +0100
    32.2 +++ b/src/ZF/ex/Bin.ML	Sat Feb 15 17:52:31 1997 +0100
    32.3 @@ -379,7 +379,7 @@
    32.4                bin_mult_Plus, bin_mult_Minus,
    32.5                bin_mult_Bcons1, bin_mult_Bcons0] @
    32.6               norm_Bcons_simps
    32.7 -    setsolver (type_auto_tac ([bool_1I, bool_0I] @ bin_typechecks0));
    32.8 +    setSolver (type_auto_tac ([bool_1I, bool_0I] @ bin_typechecks0));
    32.9  
   32.10  
   32.11  (*** Examples of performing binary arithmetic by simplification ***)
    33.1 --- a/src/ZF/ex/Primrec.ML	Sat Feb 15 17:48:19 1997 +0100
    33.2 +++ b/src/ZF/ex/Primrec.ML	Sat Feb 15 17:52:31 1997 +0100
    33.3 @@ -22,7 +22,7 @@
    33.4  
    33.5  (** Useful special cases of evaluation ***)
    33.6  
    33.7 -simpset := !simpset setsolver (type_auto_tac pr_typechecks);
    33.8 +simpset := !simpset setSolver (type_auto_tac pr_typechecks);
    33.9  
   33.10  goalw Primrec.thy [SC_def]
   33.11      "!!x l. [| x:nat;  l: list(nat) |] ==> SC ` (Cons(x,l)) = succ(x)";
   33.12 @@ -61,7 +61,7 @@
   33.13  (* c: primrec ==> c: list(nat) -> nat *)
   33.14  val primrec_into_fun = primrec.dom_subset RS subsetD;
   33.15  
   33.16 -simpset := !simpset setsolver (type_auto_tac ([primrec_into_fun] @ 
   33.17 +simpset := !simpset setSolver (type_auto_tac ([primrec_into_fun] @ 
   33.18  					      pr_typechecks @ primrec.intrs));
   33.19  
   33.20  goalw Primrec.thy [ACK_def] "!!i. i:nat ==> ACK(i): primrec";
    34.1 --- a/src/ZF/ex/TF.ML	Sat Feb 15 17:48:19 1997 +0100
    34.2 +++ b/src/ZF/ex/TF.ML	Sat Feb 15 17:52:31 1997 +0100
    34.3 @@ -202,7 +202,7 @@
    34.4      [TconsI, FnilI, FconsI, treeI, forestI,
    34.5       list_of_TF_type, TF_map_type, TF_size_type, TF_preorder_type];
    34.6  
    34.7 -simpset := !simpset setsolver type_auto_tac (list_typechecks@TF_typechecks);
    34.8 +simpset := !simpset setSolver type_auto_tac (list_typechecks@TF_typechecks);
    34.9  
   34.10  (** theorems about list_of_TF and TF_of_list **)
   34.11  
    35.1 --- a/src/ZF/ex/Term.ML	Sat Feb 15 17:48:19 1997 +0100
    35.2 +++ b/src/ZF/ex/Term.ML	Sat Feb 15 17:52:31 1997 +0100
    35.3 @@ -172,7 +172,7 @@
    35.4  (*map_type2 and term_map_type2 instantiate variables*)
    35.5  simpset := !simpset
    35.6        addsimps [term_rec, term_map, term_size, reflect, preorder]
    35.7 -      setsolver type_auto_tac (list_typechecks@term_typechecks);
    35.8 +      setSolver type_auto_tac (list_typechecks@term_typechecks);
    35.9  
   35.10  
   35.11  (** theorems about term_map **)
    36.1 --- a/src/ZF/indrule.ML	Sat Feb 15 17:48:19 1997 +0100
    36.2 +++ b/src/ZF/indrule.ML	Sat Feb 15 17:52:31 1997 +0100
    36.3 @@ -82,7 +82,7 @@
    36.4    fail.  *)
    36.5  val min_ss = empty_ss
    36.6        setmksimps (map mk_meta_eq o ZF_atomize o gen_all)
    36.7 -      setsolver  (fn prems => resolve_tac (triv_rls@prems) 
    36.8 +      setSolver  (fn prems => resolve_tac (triv_rls@prems) 
    36.9                                ORELSE' assume_tac
   36.10                                ORELSE' etac FalseE);
   36.11