# HG changeset patch
# User paulson
# Date 849808869 -3600
# Node ID 7c252931a72cdd01e198a0a18e37f968a35add10
# Parent  3ae9b0ccee21a878fd004ceb18c0ee90315d0f60
Minor speedups

diff -r 3ae9b0ccee21 -r 7c252931a72c src/HOL/Auth/NS_Public.ML
--- a/src/HOL/Auth/NS_Public.ML	Thu Dec 05 19:00:28 1996 +0100
+++ b/src/HOL/Auth/NS_Public.ML	Thu Dec 05 19:01:09 1996 +0100
@@ -155,8 +155,8 @@
 by (step_tac (!claset addSIs [impOfSubs (subset_insertI RS analz_mono)]) 1);
 by (ex_strip_tac 1);
 by (best_tac (!claset delrules [conjI]
-	              addDs  [impOfSubs analz_subset_parts,
-			      impOfSubs Fake_parts_insert]
+		      addSDs [impOfSubs Fake_parts_insert]
+	              addDs  [impOfSubs analz_subset_parts]
                       addss (!simpset)) 1);
 val lemma = result();
 
@@ -224,8 +224,8 @@
 by (fast_tac (!claset addss (!simpset)) 1);
 by (forward_tac [Spy_not_see_NA] 1 THEN REPEAT (assume_tac 1));
 by (best_tac (!claset addSIs [disjI2]
-		      addDs [impOfSubs analz_subset_parts,
-			     impOfSubs Fake_parts_insert]
+		      addSDs [impOfSubs Fake_parts_insert]
+		      addDs  [impOfSubs analz_subset_parts]
 	              addss (!simpset)) 1);
 qed_spec_mp "NA_decrypt_imp_B_msg";
 
@@ -256,9 +256,9 @@
                setloop split_tac [expand_if])));
 (*Fake*)
 by (best_tac (!claset addSIs [disjI2]
-		      addIs [impOfSubs (subset_insertI RS analz_mono)]
-		      addDs [impOfSubs analz_subset_parts,
-			     impOfSubs Fake_parts_insert]
+		      addSDs [impOfSubs Fake_parts_insert]
+		      addIs  [impOfSubs (subset_insertI RS analz_mono)]
+		      addDs  [impOfSubs analz_subset_parts]
 	              addss (!simpset)) 2);
 (*Base*)
 by (fast_tac (!claset addss (!simpset)) 1);
@@ -292,9 +292,9 @@
 by (step_tac (!claset addSIs [impOfSubs (subset_insertI RS analz_mono)]) 1);
 by (ex_strip_tac 1);
 by (best_tac (!claset delrules [conjI]
-	              addDs  [impOfSubs analz_subset_parts,
-			      impOfSubs Fake_parts_insert]
-                      addss (!simpset)) 1);
+	              addSDs [impOfSubs Fake_parts_insert]
+	              addDs  [impOfSubs analz_subset_parts] 
+	              addss (!simpset)) 1);
 val lemma = result();
 
 goal thy 
@@ -368,8 +368,8 @@
 by (fast_tac (!claset addss (!simpset)) 1);
 by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
 by (best_tac (!claset addSIs [disjI2]
-		      addDs [impOfSubs analz_subset_parts,
-			     impOfSubs Fake_parts_insert]
+		      addSDs [impOfSubs Fake_parts_insert]
+	              addDs  [impOfSubs analz_subset_parts] 
 	              addss (!simpset)) 1);
 (*NS3*)
 by (Step_tac 1);
@@ -378,7 +378,7 @@
 	              addDs  [unique_NB]) 1);
 qed_spec_mp "NB_decrypt_imp_A_msg";
 
-(*Corollary: if B receives message NS3 and the nonce NB agrees
+(*Corollary: if B receives message NS3 and the nonce NB agrees,
   then that message really originated with A.*)
 goal thy 
  "!!evs. [| Says A' B (Crypt (pubK B) (Nonce NB)): set_of_list evs;    \
diff -r 3ae9b0ccee21 -r 7c252931a72c src/HOL/Auth/NS_Public_Bad.ML
--- a/src/HOL/Auth/NS_Public_Bad.ML	Thu Dec 05 19:00:28 1996 +0100
+++ b/src/HOL/Auth/NS_Public_Bad.ML	Thu Dec 05 19:01:09 1996 +0100
@@ -160,8 +160,8 @@
 by (step_tac (!claset addSIs [impOfSubs (subset_insertI RS analz_mono)]) 1);
 by (ex_strip_tac 1);
 by (best_tac (!claset delrules [conjI]
-	              addDs  [impOfSubs analz_subset_parts,
-			      impOfSubs Fake_parts_insert]
+		      addSDs [impOfSubs Fake_parts_insert]
+	              addDs  [impOfSubs analz_subset_parts]
                       addss (!simpset)) 1);
 val lemma = result();
 
@@ -226,8 +226,9 @@
 by (REPEAT_FIRST (resolve_tac [impI, conjI]));
 by (fast_tac (!claset addss (!simpset)) 1);
 by (forward_tac [Spy_not_see_NA] 1 THEN REPEAT (assume_tac 1));
-by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
-			     impOfSubs Fake_parts_insert]
+by (best_tac (!claset addSIs [disjI2]
+		      addSDs [impOfSubs Fake_parts_insert]
+		      addDs  [impOfSubs analz_subset_parts]
 	              addss (!simpset)) 1);
 (*NS2*)
 by (Step_tac 1);
@@ -261,9 +262,9 @@
                setloop split_tac [expand_if])));
 (*Fake*)
 by (best_tac (!claset addSIs [disjI2]
-		      addIs [impOfSubs (subset_insertI RS analz_mono)]
-		      addDs [impOfSubs analz_subset_parts,
-			     impOfSubs Fake_parts_insert]
+		      addSDs [impOfSubs Fake_parts_insert]
+		      addIs  [impOfSubs (subset_insertI RS analz_mono)]
+		      addDs  [impOfSubs analz_subset_parts]
 	              addss (!simpset)) 2);
 (*Base*)
 by (fast_tac (!claset addss (!simpset)) 1);
@@ -278,7 +279,7 @@
 goal thy 
  "!!evs. evs : ns_public                                                    \
 \ ==> Nonce NB ~: analz (sees lost Spy evs) -->                             \
-\     (EX A' NA'. ALL A NA.                                                   \
+\     (EX A' NA'. ALL A NA.                                                 \
 \      Crypt (pubK A) {|Nonce NA, Nonce NB|} : parts (sees lost Spy evs) --> \
 \      A=A' & NA=NA')";
 by (etac ns_public.induct 1);
@@ -296,9 +297,9 @@
 by (step_tac (!claset addSIs [impOfSubs (subset_insertI RS analz_mono)]) 1);
 by (ex_strip_tac 1);
 by (best_tac (!claset delrules [conjI]
-	              addDs  [impOfSubs analz_subset_parts,
-			      impOfSubs Fake_parts_insert]
-                      addss (!simpset)) 1);
+	              addSDs [impOfSubs Fake_parts_insert]
+	              addDs  [impOfSubs analz_subset_parts] 
+	              addss (!simpset)) 1);
 val lemma = result();
 
 goal thy 
@@ -376,7 +377,6 @@
 br (ccontr RS disjI2) 1;
 by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
 by (Fast_tac 1);
-(*37 seconds??*)
 by (best_tac (!claset addSDs [impOfSubs Fake_parts_insert]
 	              addDs  [impOfSubs analz_subset_parts] 
 	              addss (!simpset)) 1);