# HG changeset patch
# User paulson
# Date 931433921 -7200
# Node ID 4ab8e31a842152de843848e44afbb03f9b5d97f2
# Parent  ad689270a265a58531d78b032373626dd78875f3
Now if_weak_cong is a standard congruence rule

diff -r ad689270a265 -r 4ab8e31a8421 src/HOL/Auth/Message.ML
--- a/src/HOL/Auth/Message.ML	Thu Jul 08 13:37:40 1999 +0200
+++ b/src/HOL/Auth/Message.ML	Thu Jul 08 13:38:41 1999 +0200
@@ -906,7 +906,7 @@
 fun ex_strip_tac i = REPEAT (swap_res_tac [exI, conjI] i) THEN 
                      assume_tac (i+1);
 
-(*Apply the EX-ALL quantifification to prove uniqueness theorems in 
+(*Apply the EX-ALL quantification to prove uniqueness theorems in 
   their standard form*)
 fun prove_unique_tac lemma = 
   EVERY' [dtac lemma,
diff -r ad689270a265 -r 4ab8e31a8421 src/HOL/Auth/OtwayRees_AN.ML
--- a/src/HOL/Auth/OtwayRees_AN.ML	Thu Jul 08 13:37:40 1999 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.ML	Thu Jul 08 13:38:41 1999 +0200
@@ -241,7 +241,7 @@
 by (etac otway.induct 1);
 by analz_knows_Spy_tac;
 by (ALLGOALS
-    (asm_simp_tac (simpset() addcongs [conj_cong, if_weak_cong] 
+    (asm_simp_tac (simpset() addcongs [conj_cong] 
                              addsimps [analz_insert_eq, analz_insert_freshK]
                                       @ pushes @ split_ifs)));
 (*Oops*)
diff -r ad689270a265 -r 4ab8e31a8421 src/HOL/Auth/Public.ML
--- a/src/HOL/Auth/Public.ML	Thu Jul 08 13:37:40 1999 +0200
+++ b/src/HOL/Auth/Public.ML	Thu Jul 08 13:38:41 1999 +0200
@@ -168,11 +168,10 @@
 (*Reverse the normal simplification of "image" to build up (not break down)
   the set of keys.  Based on analz_image_freshK_ss, but simpler.*)
 val analz_image_keys_ss = 
-     simpset() addcongs [if_weak_cong]
-	      delsimps [image_insert, image_Un]
-              delsimps [imp_disjL]    (*reduces blow-up*)
-              addsimps [image_insert RS sym, image_Un RS sym,
-			rangeI, 
-			insert_Key_singleton, 
-			insert_Key_image, Un_assoc RS sym];
+     simpset() delsimps [image_insert, image_Un]
+	       delsimps [imp_disjL]    (*reduces blow-up*)
+	       addsimps [image_insert RS sym, image_Un RS sym,
+			 rangeI, 
+			 insert_Key_singleton, 
+			 insert_Key_image, Un_assoc RS sym];
 
diff -r ad689270a265 -r 4ab8e31a8421 src/HOL/Auth/Shared.ML
--- a/src/HOL/Auth/Shared.ML	Thu Jul 08 13:37:40 1999 +0200
+++ b/src/HOL/Auth/Shared.ML	Thu Jul 08 13:38:41 1999 +0200
@@ -235,14 +235,13 @@
   the set of keys.  Use analz_insert_eq with (Un_upper2 RS analz_mono) to
   erase occurrences of forwarded message components (X).*)
 val analz_image_freshK_ss = 
-     simpset() addcongs [if_weak_cong]
-	      delsimps [image_insert, image_Un]
-              delsimps [imp_disjL]    (*reduces blow-up*)
-              addsimps [image_insert RS sym, image_Un RS sym,
-			analz_insert_eq, impOfSubs (Un_upper2 RS analz_mono),
-			insert_Key_singleton, subset_Compl_range,
-			Key_not_used, insert_Key_image, Un_assoc RS sym]
-                       @disj_comms;
+     simpset() delsimps [image_insert, image_Un]
+	       delsimps [imp_disjL]    (*reduces blow-up*)
+	       addsimps [image_insert RS sym, image_Un RS sym,
+			 analz_insert_eq, impOfSubs (Un_upper2 RS analz_mono),
+			 insert_Key_singleton, subset_Compl_range,
+			 Key_not_used, insert_Key_image, Un_assoc RS sym]
+			@disj_comms;
 
 (*Lemma for the trivial direction of the if-and-only-if*)
 Goal "(Key K : analz (Key``nE Un H)) --> (K : nE | Key K : analz H)  ==> \
diff -r ad689270a265 -r 4ab8e31a8421 src/HOL/Auth/TLS.ML
--- a/src/HOL/Auth/TLS.ML	Thu Jul 08 13:37:40 1999 +0200
+++ b/src/HOL/Auth/TLS.ML	Thu Jul 08 13:38:41 1999 +0200
@@ -176,14 +176,10 @@
 fun analz_induct_tac i = 
     etac tls.induct i   THEN
     ClientKeyExch_tac  (i+6)  THEN	(*ClientKeyExch*)
-    ALLGOALS (asm_simp_tac 
-              (simpset() addcongs [if_weak_cong]
-                         addsimps split_ifs @ pushes))  THEN
+    ALLGOALS (asm_simp_tac (simpset() addsimps split_ifs @ pushes))  THEN
     (*Remove instances of pubK B:  the Spy already knows all public keys.
       Combining the two simplifier calls makes them run extremely slowly.*)
-    ALLGOALS (asm_simp_tac 
-              (simpset() addcongs [if_weak_cong]
-			 addsimps [insert_absorb]));
+    ALLGOALS (asm_simp_tac (simpset() addsimps [insert_absorb]));
 
 
 (*** Properties of items found in Notes ***)
diff -r ad689270a265 -r 4ab8e31a8421 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Thu Jul 08 13:37:40 1999 +0200
+++ b/src/HOL/simpdata.ML	Thu Jul 08 13:38:41 1999 +0200
@@ -483,8 +483,7 @@
 
 (* install implicit simpset *)
 
-simpset_ref() := HOL_ss;
-
+simpset_ref() := HOL_ss addcongs [if_weak_cong];
 
 
 (*** integration of simplifier with classical reasoner ***)