# HG changeset patch
# User paulson
# Date 874507114 -7200
# Node ID 7588653475b2303ee85bbc8dc06349c55760aadd
# Parent  8df171ccdbd8e004e3b7057b18323b5c19dcd6ca
Removed the simprule imp_disjL from the analz_image_..._ss to boost speed

diff -r 8df171ccdbd8 -r 7588653475b2 src/HOL/Auth/Public.ML
--- a/src/HOL/Auth/Public.ML	Wed Sep 17 16:37:40 1997 +0200
+++ b/src/HOL/Auth/Public.ML	Wed Sep 17 16:38:34 1997 +0200
@@ -115,8 +115,7 @@
 (*Inductive step*)
 by (induct_tac "a" 1);
 by (ALLGOALS (full_simp_tac 
-	      (!simpset delsimps [sees_Notes]
-		        addsimps [UN_parts_sees_Says,
+	      (!simpset addsimps [UN_parts_sees_Says,
 				  UN_parts_sees_Notes])));
 by (ALLGOALS (rtac (msg_Nonce_supply RS exE)));
 by (ALLGOALS (blast_tac (!claset addSEs [add_leE])));
@@ -152,6 +151,7 @@
 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, 
diff -r 8df171ccdbd8 -r 7588653475b2 src/HOL/Auth/Shared.ML
--- a/src/HOL/Auth/Shared.ML	Wed Sep 17 16:37:40 1997 +0200
+++ b/src/HOL/Auth/Shared.ML	Wed Sep 17 16:38:34 1997 +0200
@@ -113,8 +113,7 @@
 (*Inductive step*)
 by (induct_tac "a" 1);
 by (ALLGOALS (full_simp_tac 
-	      (!simpset delsimps [sees_Notes]
-		        addsimps [UN_parts_sees_Says,
+	      (!simpset addsimps [UN_parts_sees_Says,
 				  UN_parts_sees_Notes])));
 by (ALLGOALS (rtac (msg_Nonce_supply RS exE)));
 by (ALLGOALS (blast_tac (!claset addSEs [add_leE])));
@@ -235,6 +234,7 @@
 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,