--- 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,
--- 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,