--- a/src/HOL/Auth/Message.ML Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/Auth/Message.ML Sat Feb 15 17:52:31 1997 +0100
@@ -825,13 +825,6 @@
(*Cannot be added with Addsimps -- we don't always want to re-order messages*)
val pushes = pushKeys@pushCrypts;
-
-(*No premature instantiation of variables during simplification.
- For proving "possibility" properties.*)
-fun safe_solver prems =
- match_tac (TrueI::refl::prems) ORELSE' eq_assume_tac
- ORELSE' etac FalseE;
-
val Fake_insert_tac =
dresolve_tac [impOfSubs Fake_analz_insert,
impOfSubs Fake_parts_insert] THEN'
--- a/src/HOL/Auth/NS_Public.ML Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/Auth/NS_Public.ML Sat Feb 15 17:52:31 1997 +0100
@@ -12,6 +12,8 @@
proof_timing:=true;
HOL_quantifiers := false;
+val op addss = op unsafe_addss;
+
AddIffs [Spy_in_lost];
(*Replacing the variable by a constant improves search speed by 50%!*)
--- a/src/HOL/Auth/NS_Public_Bad.ML Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/Auth/NS_Public_Bad.ML Sat Feb 15 17:52:31 1997 +0100
@@ -16,6 +16,8 @@
proof_timing:=true;
HOL_quantifiers := false;
+val op addss = op unsafe_addss;
+
AddIffs [Spy_in_lost];
(*Replacing the variable by a constant improves search speed by 50%!*)
--- a/src/HOL/Auth/NS_Shared.ML Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/Auth/NS_Shared.ML Sat Feb 15 17:52:31 1997 +0100
@@ -113,7 +113,7 @@
(!claset addIs [impOfSubs analz_subset_parts]
addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
- addss (!simpset)) 1);
+ unsafe_addss (!simpset)) 1);
(*NS2, NS4, NS5*)
by (REPEAT (fast_tac (!claset addSEs sees_Spy_partsEs addss (!simpset)) 1));
qed_spec_mp "new_keys_not_used";
@@ -167,7 +167,7 @@
\ | X : analz (sees lost Spy evs)";
by (case_tac "A : lost" 1);
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
- addss (!simpset)) 1);
+ unsafe_addss (!simpset)) 1);
by (forward_tac [Says_imp_sees_Spy RS parts.Inj] 1);
by (fast_tac (!claset addEs partsEs
addSDs [A_trusts_NS2, Says_Server_message_form]
--- a/src/HOL/Auth/OtwayRees.ML Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/Auth/OtwayRees.ML Sat Feb 15 17:52:31 1997 +0100
@@ -92,9 +92,9 @@
(*Fake message*)
TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
impOfSubs Fake_parts_insert]
- addss (!simpset)) 2)) THEN
+ unsafe_addss (!simpset)) 2)) THEN
(*Base case*)
- fast_tac (!claset addss (!simpset)) 1 THEN
+ fast_tac (!claset unsafe_addss (!simpset)) 1 THEN
ALLGOALS Asm_simp_tac) i;
(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
@@ -134,7 +134,7 @@
(!claset addIs [impOfSubs analz_subset_parts]
addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
- addss (!simpset)) 1);
+ unsafe_addss (!simpset)) 1);
(*OR1-3*)
by (REPEAT (fast_tac (!claset addss (!simpset)) 1));
qed_spec_mp "new_keys_not_used";
--- a/src/HOL/Auth/OtwayRees_AN.ML Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/Auth/OtwayRees_AN.ML Sat Feb 15 17:52:31 1997 +0100
@@ -123,7 +123,7 @@
(!claset addIs [impOfSubs analz_subset_parts]
addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
- addss (!simpset)) 1);
+ unsafe_addss (!simpset)) 1);
(*OR3*)
by (fast_tac (!claset addss (!simpset)) 1);
qed_spec_mp "new_keys_not_used";
@@ -297,7 +297,7 @@
addIs [impOfSubs analz_subset_parts]
addss (!simpset addsimps [parts_insert2])) 2);
(*Oops*)
-by (best_tac (!claset addDs [unique_session_keys] addss (!simpset)) 3);
+by (best_tac (!claset addDs [unique_session_keys] unsafe_addss (!simpset)) 3);
(*OR4, Fake*)
by (REPEAT_FIRST spy_analz_tac);
val lemma = result() RS mp RS mp RSN(2,rev_notE);
--- a/src/HOL/Auth/OtwayRees_Bad.ML Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.ML Sat Feb 15 17:52:31 1997 +0100
@@ -125,7 +125,7 @@
(!claset addIs [impOfSubs analz_subset_parts]
addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
- addss (!simpset)) 1);
+ unsafe_addss (!simpset)) 1);
(*OR1-3*)
by (REPEAT (fast_tac (!claset addss (!simpset)) 1));
qed_spec_mp "new_keys_not_used";
--- a/src/HOL/Auth/Public.ML Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/Auth/Public.ML Sat Feb 15 17:52:31 1997 +0100
@@ -186,7 +186,7 @@
by (fast_tac (!claset addSEs [add_leE]) 2);
(*Nonce case*)
by (res_inst_tac [("x","N + Suc nat")] exI 1);
-by (fast_tac (!claset addSEs [add_leE] addafter (TRYALL trans_tac)) 1);
+by (fast_tac (!claset addSEs [add_leE] addaltern trans_tac) 1);
val lemma = result();
goal thy "Nonce (@ N. Nonce N ~: used evs) ~: used evs";
@@ -198,7 +198,7 @@
(*Tactic for possibility theorems*)
val possibility_tac =
REPEAT
- (ALLGOALS (simp_tac (!simpset setsolver safe_solver))
+ (ALLGOALS (simp_tac (!simpset setSolver safe_solver))
THEN
REPEAT_FIRST (eq_assume_tac ORELSE'
resolve_tac [refl, conjI, Nonce_supply]));
--- a/src/HOL/Auth/Recur.ML Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/Auth/Recur.ML Sat Feb 15 17:52:31 1997 +0100
@@ -157,9 +157,9 @@
(*Fake message*)
TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
impOfSubs Fake_parts_insert]
- addss (!simpset)) 2)) THEN
+ unsafe_addss (!simpset)) 2)) THEN
(*Base case*)
- fast_tac (!claset addss (!simpset)) 1 THEN
+ fast_tac (!claset unsafe_addss (!simpset)) 1 THEN
ALLGOALS Asm_simp_tac) i;
(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
@@ -178,7 +178,7 @@
addss (!simpset addsimps [parts_insert_sees])) 2);
(*RA2*)
by (best_tac (!claset addSEs partsEs addSDs [parts_cut]
- addss (!simpset)) 1);
+ unsafe_addss (!simpset)) 1);
qed "Spy_see_shrK";
Addsimps [Spy_see_shrK];
@@ -215,13 +215,13 @@
by (parts_induct_tac 1);
(*RA3*)
by (best_tac (!claset addDs [Key_in_keysFor_parts]
- addss (!simpset addsimps [parts_insert_sees])) 2);
+ unsafe_addss (!simpset addsimps [parts_insert_sees])) 2);
(*Fake*)
by (best_tac
(!claset addIs [impOfSubs analz_subset_parts]
addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
- addss (!simpset)) 1);
+ unsafe_addss (!simpset)) 1);
qed_spec_mp "new_keys_not_used";
@@ -574,5 +574,5 @@
addSIs [disjI2]
addSEs [MPair_parts]
addDs [parts.Body]
- addss (!simpset)) 0 1);
+ unsafe_addss (!simpset)) 0 1);
qed "Cert_imp_Server_msg";
--- a/src/HOL/Auth/Shared.ML Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/Auth/Shared.ML Sat Feb 15 17:52:31 1997 +0100
@@ -140,7 +140,7 @@
by (Step_tac 1);
by (etac rev_mp 1); (*split_tac does not work on assumptions*)
by (ALLGOALS
- (fast_tac (!claset addss (!simpset addsimps [parts_Un, sees_Cons]
+ (fast_tac (!claset unsafe_addss (!simpset addsimps [parts_Un, sees_Cons]
setloop split_tac [expand_if]))));
qed "UN_parts_sees_Says";
@@ -157,7 +157,7 @@
"!!evs. [| Says A B (Crypt (shrK C) X) : set_of_list evs; C : lost |] \
\ ==> X : analz (sees lost Spy evs)";
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
- addss (!simpset)) 1);
+ unsafe_addss (!simpset)) 1);
qed "Says_Crypt_lost";
goal thy
@@ -165,7 +165,7 @@
\ X ~: analz (sees lost Spy evs) |] \
\ ==> C ~: lost";
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
- addss (!simpset)) 1);
+ unsafe_addss (!simpset)) 1);
qed "Says_Crypt_not_lost";
(*NEEDED??*)
@@ -267,7 +267,7 @@
by (fast_tac (!claset addSEs [add_leE]) 2);
(*Nonce case*)
by (res_inst_tac [("x","N + Suc nat")] exI 1);
-by (fast_tac (!claset addSEs [add_leE] addafter (TRYALL trans_tac)) 1);
+by (fast_tac (!claset addSEs [add_leE] addaltern trans_tac) 1);
val lemma = result();
goal thy "EX N. Nonce N ~: used evs";
@@ -352,7 +352,7 @@
val possibility_tac =
REPEAT (*omit used_Says so that Nonces, Keys start from different traces!*)
(ALLGOALS (simp_tac
- (!simpset delsimps [used_Says] setsolver safe_solver))
+ (!simpset delsimps [used_Says] setSolver safe_solver))
THEN
REPEAT_FIRST (eq_assume_tac ORELSE'
resolve_tac [refl, conjI, Nonce_supply, Key_supply]));
@@ -361,7 +361,7 @@
nonces and keys initially*)
val basic_possibility_tac =
REPEAT
- (ALLGOALS (asm_simp_tac (!simpset setsolver safe_solver))
+ (ALLGOALS (asm_simp_tac (!simpset setSolver safe_solver))
THEN
REPEAT_FIRST (resolve_tac [refl, conjI]));
--- a/src/HOL/Auth/WooLam.ML Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/Auth/WooLam.ML Sat Feb 15 17:52:31 1997 +0100
@@ -26,10 +26,10 @@
by (REPEAT (resolve_tac [exI,bexI] 1));
by (rtac (woolam.Nil RS woolam.WL1 RS woolam.WL2 RS woolam.WL3 RS
woolam.WL4 RS woolam.WL5) 2);
-by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
+by (ALLGOALS (simp_tac (!simpset setSolver safe_solver)));
by (REPEAT_FIRST (resolve_tac [refl, conjI]));
by (REPEAT_FIRST (fast_tac (!claset addSEs [Nonce_supply RS notE]
- addss (!simpset setsolver safe_solver))));
+ addss (!simpset setSolver safe_solver))));
result();
--- a/src/HOL/Auth/Yahalom.ML Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/Auth/Yahalom.ML Sat Feb 15 17:52:31 1997 +0100
@@ -16,6 +16,8 @@
HOL_quantifiers := false;
Pretty.setdepth 25;
+val op addss = op unsafe_addss;
+
(*A "possibility property": there are traces that reach the end*)
goal thy
--- a/src/HOL/Auth/Yahalom2.ML Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/Auth/Yahalom2.ML Sat Feb 15 17:52:31 1997 +0100
@@ -17,6 +17,7 @@
proof_timing:=true;
HOL_quantifiers := false;
+val op addss = op unsafe_addss;
(*A "possibility property": there are traces that reach the end*)
goal thy
--- a/src/HOL/IMP/Transition.ML Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/IMP/Transition.ML Sat Feb 15 17:52:31 1997 +0100
@@ -201,7 +201,7 @@
"(c,s) -*-> (c',s') ==> <c',s'> -c-> t --> <c,s> -c-> t";
by (rtac (major RS rtrancl_induct2) 1);
by (Fast_tac 1);
-by (fast_tac (!claset addIs [FB_lemma3] addbefore (split_all_tac 1)) 1);
+by (fast_tac (!claset addIs [FB_lemma3] addbefore split_all_tac) 1);
qed_spec_mp "FB_lemma2";
goal Transition.thy "!!c. (c,s) -*-> (SKIP,t) ==> <c,s> -c-> t";
--- a/src/HOL/Lambda/Lambda.ML Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/Lambda/Lambda.ML Sat Feb 15 17:52:31 1997 +0100
@@ -66,7 +66,7 @@
"!i k. i < Suc k --> lift (lift t i) (Suc k) = lift (lift t k) i";
by (dB.induct_tac "t" 1);
by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])
- addsolver (cut_trans_tac))));
+ addSolver cut_trans_tac)));
by (safe_tac HOL_cs);
by (ALLGOALS trans_tac);
qed_spec_mp "lift_lift";
@@ -76,7 +76,7 @@
by (dB.induct_tac "t" 1);
by (ALLGOALS(asm_simp_tac (!simpset addsimps [pred_def,subst_Var,lift_lift]
setloop (split_tac [expand_if,expand_nat_case])
- addsolver (cut_trans_tac))));
+ addSolver cut_trans_tac)));
by (safe_tac HOL_cs);
by (ALLGOALS trans_tac);
qed "lift_subst";
@@ -88,7 +88,7 @@
by (dB.induct_tac "t" 1);
by (ALLGOALS(asm_simp_tac (!simpset addsimps [subst_Var,lift_lift]
setloop (split_tac [expand_if])
- addsolver (cut_trans_tac))));
+ addSolver cut_trans_tac)));
by(safe_tac (HOL_cs addSEs [nat_neqE]));
by(ALLGOALS trans_tac);
qed "lift_subst_lt";
@@ -106,7 +106,7 @@
by (ALLGOALS(asm_simp_tac
(!simpset addsimps [pred_def,subst_Var,lift_lift RS sym,lift_subst_lt]
setloop (split_tac [expand_if,expand_nat_case])
- addsolver (cut_trans_tac))));
+ addSolver cut_trans_tac)));
by(safe_tac (HOL_cs addSEs [nat_neqE]));
by(ALLGOALS trans_tac);
qed_spec_mp "subst_subst";
--- a/src/HOL/Lambda/ParRed.ML Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/Lambda/ParRed.ML Sat Feb 15 17:52:31 1997 +0100
@@ -83,7 +83,7 @@
by (Simp_tac 1);
by (etac rev_mp 1);
by (dB.induct_tac "dB1" 1);
- by (ALLGOALS(fast_tac (!claset addSIs [par_beta_subst] addss !simpset)));
+ by (ALLGOALS(fast_tac (!claset addSIs [par_beta_subst] unsafe_addss (!simpset))));
qed_spec_mp "par_beta_cd";
(*** Confluence (via cd) ***)
--- a/src/HOL/MiniML/W.ML Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/MiniML/W.ML Sat Feb 15 17:52:31 1997 +0100
@@ -492,7 +492,7 @@
by (eres_inst_tac [("x","(FVar n)#A")] allE 1);
by (eres_inst_tac [("x","t2")] allE 1);
by (eres_inst_tac [("x","Suc n")] allE 1);
-by (best_tac (HOL_cs addSDs [mk_scheme_injective] addss (!simpset addcongs [conj_cong]
+by (best_tac (HOL_cs addSDs [mk_scheme_injective] unsafe_addss (!simpset addcongs [conj_cong]
setloop (split_tac [expand_option_bind]))) 1);
(* case App e1 e2 *)
--- a/src/HOL/Prod.ML Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/Prod.ML Sat Feb 15 17:52:31 1997 +0100
@@ -78,7 +78,7 @@
end;
goal Prod.thy "(!x. P x) = (!a b. P(a,b))";
-by (fast_tac (!claset addbefore split_all_tac 1) 1);
+by (fast_tac (!claset addbefore split_all_tac) 1);
qed "split_paired_All";
goalw Prod.thy [split_def] "split c (a,b) = c a b";
--- a/src/HOL/Relation.ML Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/Relation.ML Sat Feb 15 17:52:31 1997 +0100
@@ -173,11 +173,11 @@
(REPEAT (eresolve_tac [asm_rl, ImageE, subsetD RS SigmaD2] 1)) ]);
goal Relation.thy "R O id = R";
-by (fast_tac (!claset addbefore (split_all_tac 1)) 1);
+by (fast_tac (!claset addbefore split_all_tac) 1);
qed "R_O_id";
goal Relation.thy "id O R = R";
-by (fast_tac (!claset addbefore (split_all_tac 1)) 1);
+by (fast_tac (!claset addbefore split_all_tac) 1);
qed "id_O_R";
Addsimps [R_O_id,id_O_R];
--- a/src/HOL/W0/I.ML Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/W0/I.ML Sat Feb 15 17:52:31 1997 +0100
@@ -8,6 +8,8 @@
open I;
+val op addss = op unsafe_addss;
+
goal thy
"! a m s s' t n. \
\ (new_tv m a & new_tv m s) --> I e a m s = Ok(s',t,n) --> \
--- a/src/HOL/W0/Type.ML Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/W0/Type.ML Sat Feb 15 17:52:31 1997 +0100
@@ -259,7 +259,7 @@
(* case [] *)
by (Simp_tac 1);
(* case x#xl *)
-by (fast_tac (set_cs addss (!simpset setloop (split_tac [expand_if]))) 1);
+by (fast_tac (set_cs unsafe_addss(!simpset setloop (split_tac [expand_if]))) 1);
qed_spec_mp "ftv_mem_sub_ftv_list";
Addsimps [ftv_mem_sub_ftv_list];
--- a/src/HOL/W0/W.ML Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/W0/W.ML Sat Feb 15 17:52:31 1997 +0100
@@ -45,7 +45,7 @@
"!a n s t m. W e a n = Ok (s,t,m) --> n<=m";
by (expr.induct_tac "e" 1);
(* case Var(n) *)
-by (fast_tac (HOL_cs addss (!simpset setloop (split_tac [expand_if]))) 1);
+by (fast_tac (HOL_cs unsafe_addss(!simpset setloop (split_tac [expand_if]))) 1);
(* case Abs e *)
by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
by (fast_tac (HOL_cs addDs [Suc_leD]) 1);
@@ -91,7 +91,7 @@
\ new_tv m s & new_tv m t";
by (expr.induct_tac "e" 1);
(* case Var n *)
-by (fast_tac (HOL_cs addss (!simpset
+by (fast_tac (HOL_cs unsafe_addss (!simpset
addsimps [id_subst_def,list_all_nth,new_tv_list,new_tv_subst]
setloop (split_tac [expand_if]))) 1);
@@ -161,7 +161,7 @@
by (expr.induct_tac "e" 1);
(* case Var n *)
by (fast_tac (HOL_cs addIs [nth_mem,subsetD,ftv_mem_sub_ftv_list]
- addss (!simpset setloop (split_tac [expand_if]))) 1);
+ unsafe_addss (!simpset setloop (split_tac [expand_if]))) 1);
(* case Abs e *)
by (asm_full_simp_tac (!simpset addsimps
--- a/src/HOL/WF.ML Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/WF.ML Sat Feb 15 17:52:31 1997 +0100
@@ -90,7 +90,7 @@
(cut_facts_tac hyps THEN'
DEPTH_SOLVE_1 o (ares_tac [TrueI] ORELSE'
eresolve_tac [transD, mp, allE]));
-val wf_super_ss = HOL_ss addsolver indhyp_tac;
+val wf_super_ss = HOL_ss addSolver indhyp_tac;
val prems = goalw WF.thy [is_recfun_def,cut_def]
"[| wf(r); trans(r); is_recfun r H a f; is_recfun r H b g |] ==> \
--- a/src/HOL/ex/Comb.ML Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/ex/Comb.ML Sat Feb 15 17:52:31 1997 +0100
@@ -55,7 +55,7 @@
AddIs contract.intrs;
AddSEs [K_contractE, S_contractE, Ap_contractE];
-Addss (!simpset);
+Unsafe_Addss (!simpset);
goalw Comb.thy [I_def] "!!z. I -1-> z ==> P";
by (Fast_tac 1);
@@ -106,7 +106,7 @@
AddIs parcontract.intrs;
AddSEs [K_parcontractE, S_parcontractE,Ap_parcontractE];
-Addss (!simpset);
+Unsafe_Addss (!simpset);
(*** Basic properties of parallel contraction ***)
--- a/src/HOL/indrule.ML Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/indrule.ML Sat Feb 15 17:52:31 1997 +0100
@@ -85,10 +85,7 @@
simplifications. If the premises get simplified, then the proofs will
fail. This arose with a premise of the form {(F n,G n)|n . True}, which
expanded to something containing ...&True. *)
-val min_ss = empty_ss
- setmksimps (mksimps mksimps_pairs)
- setsolver (fn prems => resolve_tac (TrueI::refl::prems) ORELSE' atac
- ORELSE' etac FalseE);
+val min_ss = HOL_basic_ss;
val quant_induct =
prove_goalw_cterm part_rec_defs
--- a/src/ZF/Arith.ML Sat Feb 15 17:48:19 1997 +0100
+++ b/src/ZF/Arith.ML Sat Feb 15 17:52:31 1997 +0100
@@ -537,7 +537,7 @@
qed "zero_lt_mult_iff";
goal Arith.thy "!!k. [| m: nat; n: nat |] ==> m#*n = 1 <-> m=1 & n=1";
-by (best_tac (!claset addEs [natE] addss (!simpset)) 1);
+by (best_tac (!claset addEs [natE] unsafe_addss (!simpset)) 1);
qed "mult_eq_1_iff";
(*Cancellation law for division*)
@@ -576,7 +576,7 @@
by (rtac disjCI 1);
by (dtac sym 1);
by (rtac Ord_linear_lt 1 THEN REPEAT_SOME (ares_tac [nat_into_Ord,nat_1I]));
-by (fast_tac (!claset addss (!simpset)) 1);
+by (fast_tac (!claset unsafe_addss (!simpset)) 1);
by (fast_tac (le_cs addDs [mono_lemma]
addss (!simpset addsimps [mult_1_right])) 1);
qed "mult_eq_self_implies_10";
--- a/src/ZF/Epsilon.ML Sat Feb 15 17:48:19 1997 +0100
+++ b/src/ZF/Epsilon.ML Sat Feb 15 17:52:31 1997 +0100
@@ -313,7 +313,7 @@
goal thy "transrec2(succ(i),a,b) = b(i, transrec2(i,a,b))";
by (rtac (transrec2_def RS def_transrec RS trans) 1);
by (simp_tac (!simpset addsimps [succ_not_0, THE_eq, if_P]
- setsolver K Fast_tac) 1);
+ setSolver K Fast_tac) 1);
qed "transrec2_succ";
goal thy "!!i. Limit(i) ==> transrec2(i,a,b) = (UN j<i. transrec2(j,a,b))";
--- a/src/ZF/List.ML Sat Feb 15 17:48:19 1997 +0100
+++ b/src/ZF/List.ML Sat Feb 15 17:52:31 1997 +0100
@@ -259,7 +259,7 @@
[list_rec_type, map_type, map_type2, app_type, length_type,
rev_type, flat_type, list_add_type];
-simpset := !simpset setsolver (type_auto_tac list_typechecks);
+simpset := !simpset setSolver (type_auto_tac list_typechecks);
(*** theorems about map ***)
--- a/src/ZF/Order.ML Sat Feb 15 17:48:19 1997 +0100
+++ b/src/ZF/Order.ML Sat Feb 15 17:52:31 1997 +0100
@@ -11,6 +11,8 @@
open Order;
+val op addss = op unsafe_addss;
+
(** Basic properties of the definitions **)
(*needed?*)
@@ -237,11 +239,10 @@
(*Rewriting with bijections and converse (function inverse)*)
val bij_inverse_ss =
- !simpset setsolver (type_auto_tac [ord_iso_is_bij, bij_is_fun, apply_type,
+ !simpset setSolver (type_auto_tac [ord_iso_is_bij, bij_is_fun, apply_type,
bij_converse_bij, comp_fun, comp_bij])
addsimps [right_inverse_bij, left_inverse_bij];
-
(** Symmetry and Transitivity Rules **)
(*Reflexivity of similarity*)
--- a/src/ZF/Perm.ML Sat Feb 15 17:48:19 1997 +0100
+++ b/src/ZF/Perm.ML Sat Feb 15 17:52:31 1997 +0100
@@ -335,7 +335,7 @@
by (rtac lam_funtype 2);
by (typechk_tac (prem::ZF_typechecks));
by (asm_simp_tac (!simpset
- setsolver type_auto_tac [lam_type, lam_funtype, prem]) 1);
+ setSolver type_auto_tac [lam_type, lam_funtype, prem]) 1);
qed "comp_lam";
goal Perm.thy "!!f g. [| g: inj(A,B); f: inj(B,C) |] ==> (f O g) : inj(A,C)";
@@ -343,7 +343,7 @@
f_imp_injective 1);
by (REPEAT (ares_tac [comp_fun, inj_is_fun] 1));
by (asm_simp_tac (!simpset addsimps [left_inverse]
- setsolver type_auto_tac [inj_is_fun, apply_type]) 1);
+ setSolver type_auto_tac [inj_is_fun, apply_type]) 1);
qed "comp_inj";
goalw Perm.thy [surj_def]
@@ -544,7 +544,7 @@
"!!f. [| f: inj(A,B); a~:A; b~:B |] ==> \
\ cons(<a,b>,f) : inj(cons(a,A), cons(b,B))";
by (fast_tac (!claset addIs [apply_type]
- addss (!simpset addsimps [fun_extend, fun_extend_apply2,
+ unsafe_addss (!simpset addsimps [fun_extend, fun_extend_apply2,
fun_extend_apply1]) ) 1);
qed "inj_extend";
--- a/src/ZF/WF.ML Sat Feb 15 17:48:19 1997 +0100
+++ b/src/ZF/WF.ML Sat Feb 15 17:52:31 1997 +0100
@@ -225,7 +225,7 @@
eresolve_tac [underD, transD, spec RS mp]));
(*** NOTE! some simplifications need a different solver!! ***)
-val wf_super_ss = !simpset setsolver indhyp_tac;
+val wf_super_ss = !simpset setSolver indhyp_tac;
val prems = goalw WF.thy [is_recfun_def]
"[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,b,H,g) |] ==> \
--- a/src/ZF/ex/Bin.ML Sat Feb 15 17:48:19 1997 +0100
+++ b/src/ZF/ex/Bin.ML Sat Feb 15 17:52:31 1997 +0100
@@ -379,7 +379,7 @@
bin_mult_Plus, bin_mult_Minus,
bin_mult_Bcons1, bin_mult_Bcons0] @
norm_Bcons_simps
- setsolver (type_auto_tac ([bool_1I, bool_0I] @ bin_typechecks0));
+ setSolver (type_auto_tac ([bool_1I, bool_0I] @ bin_typechecks0));
(*** Examples of performing binary arithmetic by simplification ***)
--- a/src/ZF/ex/Primrec.ML Sat Feb 15 17:48:19 1997 +0100
+++ b/src/ZF/ex/Primrec.ML Sat Feb 15 17:52:31 1997 +0100
@@ -22,7 +22,7 @@
(** Useful special cases of evaluation ***)
-simpset := !simpset setsolver (type_auto_tac pr_typechecks);
+simpset := !simpset setSolver (type_auto_tac pr_typechecks);
goalw Primrec.thy [SC_def]
"!!x l. [| x:nat; l: list(nat) |] ==> SC ` (Cons(x,l)) = succ(x)";
@@ -61,7 +61,7 @@
(* c: primrec ==> c: list(nat) -> nat *)
val primrec_into_fun = primrec.dom_subset RS subsetD;
-simpset := !simpset setsolver (type_auto_tac ([primrec_into_fun] @
+simpset := !simpset setSolver (type_auto_tac ([primrec_into_fun] @
pr_typechecks @ primrec.intrs));
goalw Primrec.thy [ACK_def] "!!i. i:nat ==> ACK(i): primrec";
--- a/src/ZF/ex/TF.ML Sat Feb 15 17:48:19 1997 +0100
+++ b/src/ZF/ex/TF.ML Sat Feb 15 17:52:31 1997 +0100
@@ -202,7 +202,7 @@
[TconsI, FnilI, FconsI, treeI, forestI,
list_of_TF_type, TF_map_type, TF_size_type, TF_preorder_type];
-simpset := !simpset setsolver type_auto_tac (list_typechecks@TF_typechecks);
+simpset := !simpset setSolver type_auto_tac (list_typechecks@TF_typechecks);
(** theorems about list_of_TF and TF_of_list **)
--- a/src/ZF/ex/Term.ML Sat Feb 15 17:48:19 1997 +0100
+++ b/src/ZF/ex/Term.ML Sat Feb 15 17:52:31 1997 +0100
@@ -172,7 +172,7 @@
(*map_type2 and term_map_type2 instantiate variables*)
simpset := !simpset
addsimps [term_rec, term_map, term_size, reflect, preorder]
- setsolver type_auto_tac (list_typechecks@term_typechecks);
+ setSolver type_auto_tac (list_typechecks@term_typechecks);
(** theorems about term_map **)
--- a/src/ZF/indrule.ML Sat Feb 15 17:48:19 1997 +0100
+++ b/src/ZF/indrule.ML Sat Feb 15 17:52:31 1997 +0100
@@ -82,7 +82,7 @@
fail. *)
val min_ss = empty_ss
setmksimps (map mk_meta_eq o ZF_atomize o gen_all)
- setsolver (fn prems => resolve_tac (triv_rls@prems)
+ setSolver (fn prems => resolve_tac (triv_rls@prems)
ORELSE' assume_tac
ORELSE' etac FalseE);