--- a/src/HOL/Auth/OtwayRees.ML Thu May 15 15:51:09 1997 +0200
+++ b/src/HOL/Auth/OtwayRees.ML Thu May 15 15:51:47 1997 +0200
@@ -132,7 +132,7 @@
(!claset addIs [impOfSubs analz_subset_parts]
addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
- unsafe_addss (!simpset)) 1);
+ addss (!simpset)) 1);
by (ALLGOALS Blast_tac);
qed_spec_mp "new_keys_not_used";
--- a/src/HOL/Auth/OtwayRees_AN.ML Thu May 15 15:51:09 1997 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.ML Thu May 15 15:51:47 1997 +0200
@@ -119,7 +119,7 @@
(!claset addIs [impOfSubs analz_subset_parts]
addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
- unsafe_addss (!simpset)) 1);
+ addss (!simpset)) 1);
(*OR3*)
by (Blast_tac 1);
qed_spec_mp "new_keys_not_used";
--- a/src/HOL/Auth/OtwayRees_Bad.ML Thu May 15 15:51:09 1997 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.ML Thu May 15 15:51:47 1997 +0200
@@ -121,7 +121,7 @@
(!claset addIs [impOfSubs analz_subset_parts]
addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
- unsafe_addss (!simpset)) 1);
+ addss (!simpset)) 1);
(*OR1-3*)
by (ALLGOALS Blast_tac);
qed_spec_mp "new_keys_not_used";
--- a/src/HOL/Auth/Public.ML Thu May 15 15:51:09 1997 +0200
+++ b/src/HOL/Auth/Public.ML Thu May 15 15:51:47 1997 +0200
@@ -120,7 +120,7 @@
by (Step_tac 1);
by (etac rev_mp 1); (*split_tac does not work on assumptions*)
by (ALLGOALS
- (fast_tac (!claset unsafe_addss (!simpset addsimps [parts_Un, sees_Cons]
+ (fast_tac (!claset addss (!simpset addsimps [parts_Un, sees_Cons]
setloop split_tac [expand_if]))));
qed "UN_parts_sees_Says";
--- a/src/HOL/Auth/ROOT.ML Thu May 15 15:51:09 1997 +0200
+++ b/src/HOL/Auth/ROOT.ML Thu May 15 15:51:47 1997 +0200
@@ -12,9 +12,6 @@
proof_timing := true;
goals_limit := 1;
-(*New version of addss isn't ready--too slow*)
-val op addss = op unsafe_addss;
-
(*Shared-key protocols*)
time_use_thy "NS_Shared";
time_use_thy "OtwayRees";
--- a/src/HOL/Auth/Recur.ML Thu May 15 15:51:09 1997 +0200
+++ b/src/HOL/Auth/Recur.ML Thu May 15 15:51:47 1997 +0200
@@ -208,13 +208,13 @@
by parts_induct_tac;
(*RA3*)
by (best_tac (!claset addDs [Key_in_keysFor_parts]
- unsafe_addss (!simpset addsimps [parts_insert_sees])) 2);
+ 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)]
- unsafe_addss (!simpset)) 1);
+ addss (!simpset)) 1);
qed_spec_mp "new_keys_not_used";
--- a/src/HOL/Auth/Shared.ML Thu May 15 15:51:09 1997 +0200
+++ b/src/HOL/Auth/Shared.ML Thu May 15 15:51:47 1997 +0200
@@ -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 unsafe_addss (!simpset addsimps [parts_Un, sees_Cons]
+ (fast_tac (!claset 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]
- unsafe_addss (!simpset)) 1);
+ 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]
- unsafe_addss (!simpset)) 1);
+ addss (!simpset)) 1);
qed "Says_Crypt_not_lost";
(*NEEDED??*)
--- a/src/HOL/Induct/Comb.ML Thu May 15 15:51:09 1997 +0200
+++ b/src/HOL/Induct/Comb.ML Thu May 15 15:51:47 1997 +0200
@@ -54,7 +54,6 @@
AddSIs [contract.K, contract.S];
AddIs [contract.Ap1, contract.Ap2];
AddSEs [K_contractE, S_contractE, Ap_contractE];
-Unsafe_Addss (!simpset);
goalw Comb.thy [I_def] "!!z. I -1-> z ==> P";
by (Blast_tac 1);
@@ -105,7 +104,6 @@
AddIs parcontract.intrs;
AddSEs [K_parcontractE, S_parcontractE,Ap_parcontractE];
-Unsafe_Addss (!simpset);
(*** Basic properties of parallel contraction ***)
--- a/src/HOL/Lambda/ParRed.ML Thu May 15 15:51:09 1997 +0200
+++ b/src/HOL/Lambda/ParRed.ML Thu May 15 15:51:47 1997 +0200
@@ -86,7 +86,7 @@
by (etac rev_mp 1);
by (dB.induct_tac "dB1" 1);
by (ALLGOALS(fast_tac (!claset addSIs [par_beta_subst]
- unsafe_addss (!simpset))));
+ addss (!simpset))));
qed_spec_mp "par_beta_cd";
(*** Confluence (via cd) ***)
--- a/src/HOL/MiniML/W.ML Thu May 15 15:51:09 1997 +0200
+++ b/src/HOL/MiniML/W.ML Thu May 15 15:51:47 1997 +0200
@@ -493,7 +493,7 @@
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]
- unsafe_addss (!simpset addcongs [conj_cong]
+ addss (!simpset addcongs [conj_cong]
setloop (split_tac [expand_option_bind]))) 1);
(** LEVEL 19 **)
--- a/src/HOL/W0/I.ML Thu May 15 15:51:09 1997 +0200
+++ b/src/HOL/W0/I.ML Thu May 15 15:51:47 1997 +0200
@@ -8,8 +8,6 @@
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 Thu May 15 15:51:09 1997 +0200
+++ b/src/HOL/W0/Type.ML Thu May 15 15:51:47 1997 +0200
@@ -259,7 +259,7 @@
(* case [] *)
by (Simp_tac 1);
(* case x#xl *)
-by (fast_tac (set_cs unsafe_addss(!simpset setloop (split_tac [expand_if]))) 1);
+by (fast_tac (set_cs 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 Thu May 15 15:51:09 1997 +0200
+++ b/src/HOL/W0/W.ML Thu May 15 15:51:47 1997 +0200
@@ -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 unsafe_addss(!simpset setloop (split_tac [expand_if]))) 1);
+by (fast_tac (HOL_cs 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 addDs [list_all_nth] unsafe_addss (!simpset
+by (fast_tac (HOL_cs addDs [list_all_nth] addss (!simpset
addsimps [id_subst_def,new_tv_list,new_tv_subst]
setloop (split_tac [expand_if]))) 1);
(* case Abs e *)
@@ -160,7 +160,7 @@
by (expr.induct_tac "e" 1);
(* case Var n *)
by (fast_tac (HOL_cs addIs [nth_mem,subsetD,ftv_mem_sub_ftv_list]
- unsafe_addss (!simpset setloop (split_tac [expand_if]))) 1);
+ addss (!simpset setloop (split_tac [expand_if]))) 1);
(* case Abs e *)
by (asm_full_simp_tac (!simpset addsimps
--- a/src/ZF/Arith.ML Thu May 15 15:51:09 1997 +0200
+++ b/src/ZF/Arith.ML Thu May 15 15:51:47 1997 +0200
@@ -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] unsafe_addss (!simpset)) 1);
+by (best_tac (!claset addEs [natE] 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 unsafe_addss (!simpset)) 1);
+by (fast_tac (!claset 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/Order.ML Thu May 15 15:51:09 1997 +0200
+++ b/src/ZF/Order.ML Thu May 15 15:51:47 1997 +0200
@@ -11,8 +11,6 @@
open Order;
-val op addss = op unsafe_addss;
-
(** Basic properties of the definitions **)
(*needed?*)
--- a/src/ZF/Perm.ML Thu May 15 15:51:09 1997 +0200
+++ b/src/ZF/Perm.ML Thu May 15 15:51:47 1997 +0200
@@ -540,7 +540,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]
- unsafe_addss (!simpset addsimps [fun_extend, fun_extend_apply2,
+ addss (!simpset addsimps [fun_extend, fun_extend_apply2,
fun_extend_apply1])) 1);
qed "inj_extend";