src/HOL/Auth/NS_Public.ML

--- a/src/HOL/Auth/NS_Public.ML	Mon Nov 03 12:22:43 1997 +0100
+++ b/src/HOL/Auth/NS_Public.ML	Mon Nov 03 12:24:13 1997 +0100
@@ -59,13 +59,13 @@
 
 goal thy 
  "!!A. evs: ns_public ==> (Key (priK A) : analz (spies evs)) = (A : bad)";
-by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
+by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
 qed "Spy_analz_priK";
 Addsimps [Spy_analz_priK];
 
 goal thy  "!!A. [| Key (priK A) : parts (spies evs);       \
 \                  evs : ns_public |] ==> A:bad";
-by (blast_tac (!claset addDs [Spy_see_priK]) 1);
+by (blast_tac (claset() addDs [Spy_see_priK]) 1);
 qed "Spy_see_priK_D";
 
 bind_thm ("Spy_analz_priK_D", analz_subset_parts RS subsetD RS Spy_see_priK_D);
@@ -85,9 +85,9 @@
 by (etac rev_mp 1);
 by (parts_induct_tac 1);
 (*NS3*)
-by (blast_tac (!claset addSEs partsEs) 3);
+by (blast_tac (claset() addSEs partsEs) 3);
 (*NS2*)
-by (blast_tac (!claset addSEs partsEs) 2);
+by (blast_tac (claset() addSEs partsEs) 2);
 by (Fake_parts_insert_tac 1);
 qed "no_nonce_NS1_NS2";
 
@@ -101,9 +101,9 @@
 by (etac rev_mp 1);
 by (parts_induct_tac 1);
 by (ALLGOALS
-    (asm_simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_spies])));
+    (asm_simp_tac (simpset() addsimps [all_conj_distrib, parts_insert_spies])));
 (*NS1*)
-by (expand_case_tac "NA = ?y" 2 THEN blast_tac (!claset addSEs partsEs) 2);
+by (expand_case_tac "NA = ?y" 2 THEN blast_tac (claset() addSEs partsEs) 2);
 (*Fake*)
 by (Clarify_tac 1);
 by (ex_strip_tac 1);
@@ -124,7 +124,7 @@
 fun analz_induct_tac i = 
     etac ns_public.induct i   THEN
     ALLGOALS (asm_simp_tac 
-              (!simpset addsplits [expand_if]));
+              (simpset() addsplits [expand_if]));
 
 
 (*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
@@ -135,14 +135,14 @@
 by (etac rev_mp 1);
 by (analz_induct_tac 1);
 (*NS3*)
-by (blast_tac (!claset addDs  [Says_imp_spies RS parts.Inj]
+by (blast_tac (claset() addDs  [Says_imp_spies RS parts.Inj]
                        addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4);
 (*NS2*)
-by (blast_tac (!claset addSEs [MPair_parts]
+by (blast_tac (claset() addSEs [MPair_parts]
 		       addDs  [Says_imp_spies RS parts.Inj,
 			       parts.Body, unique_NA]) 3);
 (*NS1*)
-by (blast_tac (!claset addSEs spies_partsEs
+by (blast_tac (claset() addSEs spies_partsEs
                        addIs  [impOfSubs analz_subset_parts]) 2);
 (*Fake*)
 by (spy_analz_tac 1);
@@ -164,9 +164,9 @@
 by (etac ns_public.induct 1);
 by (ALLGOALS Asm_simp_tac);
 (*NS1*)
-by (blast_tac (!claset addSEs spies_partsEs) 2);
+by (blast_tac (claset() addSEs spies_partsEs) 2);
 (*Fake*)
-by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert]
+by (blast_tac (claset() addSDs [impOfSubs Fake_parts_insert]
                        addDs  [Spy_not_see_NA, 
 			       impOfSubs analz_subset_parts]) 1);
 qed "A_trusts_NS2";
@@ -198,9 +198,9 @@
 by (etac rev_mp 1);
 by (parts_induct_tac 1);
 by (ALLGOALS
-    (asm_simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_spies])));
+    (asm_simp_tac (simpset() addsimps [all_conj_distrib, parts_insert_spies])));
 (*NS2*)
-by (expand_case_tac "NB = ?y" 2 THEN blast_tac (!claset addSEs partsEs) 2);
+by (expand_case_tac "NB = ?y" 2 THEN blast_tac (claset() addSEs partsEs) 2);
 (*Fake*)
 by (Clarify_tac 1);
 by (ex_strip_tac 1);
@@ -228,14 +228,14 @@
 by (etac rev_mp 1);
 by (analz_induct_tac 1);
 (*NS3*)
-by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj, unique_NB]) 4);
+by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, unique_NB]) 4);
 (*NS2: by freshness and unicity of NB*)
-by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj]
+by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj]
                        addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]
                        addEs partsEs
 		       addIs [impOfSubs analz_subset_parts]) 3);
 (*NS1*)
-by (blast_tac (!claset addSEs spies_partsEs) 2);
+by (blast_tac (claset() addSEs spies_partsEs) 2);
 (*Fake*)
 by (spy_analz_tac 1);
 qed "Spy_not_see_NB";
@@ -255,12 +255,12 @@
 by (parts_induct_tac 1);
 by (ALLGOALS Clarify_tac);
 (*NS3: because NB determines A*)
-by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj, 
+by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, 
 			      Spy_not_see_NB, unique_NB]) 3);
 (*NS1: by freshness*)
-by (blast_tac (!claset addSEs spies_partsEs) 2);
+by (blast_tac (claset() addSEs spies_partsEs) 2);
 (*Fake*)
-by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert]
+by (blast_tac (claset() addSDs [impOfSubs Fake_parts_insert]
                        addDs  [Spy_not_see_NB, 
 			       impOfSubs analz_subset_parts]) 1);
 qed "B_trusts_NS3";
@@ -288,12 +288,12 @@
 by (ALLGOALS Asm_simp_tac);
 by (ALLGOALS Clarify_tac);
 (*NS3: because NB determines A*)
-by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj, 
+by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, 
 			      Spy_not_see_NB, unique_NB]) 3);
 (*NS1*)
-by (blast_tac (!claset addSEs spies_partsEs) 2);
+by (blast_tac (claset() addSEs spies_partsEs) 2);
 (*Fake*)
-by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert]
+by (blast_tac (claset() addSDs [impOfSubs Fake_parts_insert]
                        addDs  [Spy_not_see_NB, 
 			       impOfSubs analz_subset_parts]) 1);
 qed "B_trusts_protocol";