# HG changeset patch
# User oheimb
# Date 863704307 -7200
# Node ID fe79ad367d7751fd121837eb476d147e110d5212
# Parent  a3de7f32728ca443aaa31e217dc3b1c55521c765
renamed unsafe_addss to addss

diff -r a3de7f32728c -r fe79ad367d77 src/HOL/Auth/OtwayRees.ML
--- 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";
 
diff -r a3de7f32728c -r fe79ad367d77 src/HOL/Auth/OtwayRees_AN.ML
--- 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";
diff -r a3de7f32728c -r fe79ad367d77 src/HOL/Auth/OtwayRees_Bad.ML
--- 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";
diff -r a3de7f32728c -r fe79ad367d77 src/HOL/Auth/Public.ML
--- 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";
 
diff -r a3de7f32728c -r fe79ad367d77 src/HOL/Auth/ROOT.ML
--- 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";
diff -r a3de7f32728c -r fe79ad367d77 src/HOL/Auth/Recur.ML
--- 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";
 
 
diff -r a3de7f32728c -r fe79ad367d77 src/HOL/Auth/Shared.ML
--- 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??*)
diff -r a3de7f32728c -r fe79ad367d77 src/HOL/Induct/Comb.ML
--- 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 ***)
 
diff -r a3de7f32728c -r fe79ad367d77 src/HOL/Lambda/ParRed.ML
--- 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) ***)
diff -r a3de7f32728c -r fe79ad367d77 src/HOL/MiniML/W.ML
--- 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 **)
 
diff -r a3de7f32728c -r fe79ad367d77 src/HOL/W0/I.ML
--- 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) -->   \
diff -r a3de7f32728c -r fe79ad367d77 src/HOL/W0/Type.ML
--- 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];
 
diff -r a3de7f32728c -r fe79ad367d77 src/HOL/W0/W.ML
--- 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
diff -r a3de7f32728c -r fe79ad367d77 src/ZF/Arith.ML
--- 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";
diff -r a3de7f32728c -r fe79ad367d77 src/ZF/Order.ML
--- 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?*)
diff -r a3de7f32728c -r fe79ad367d77 src/ZF/Perm.ML
--- 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";