--- 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,
--- 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*)
--- 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];
--- 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) ==> \
--- 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 ***)
--- 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 ***)