--- a/src/HOL/Auth/Kerberos_BAN.ML Tue Sep 22 17:08:30 1998 +0200
+++ b/src/HOL/Auth/Kerberos_BAN.ML Wed Sep 23 10:03:32 1998 +0200
@@ -240,8 +240,8 @@
by (etac kerberos_ban.induct 1);
by analz_spies_tac;
by (ALLGOALS
- (asm_simp_tac (simpset() addsimps ([analz_insert_eq, analz_insert_freshK]
- @ pushes))));
+ (asm_simp_tac (simpset() addsimps [analz_insert_eq, analz_insert_freshK]
+ @ pushes)));
(*Oops*)
by (blast_tac (claset() addDs [unique_session_keys] addIs [less_SucI]) 4);
(*Kb2*)
--- a/src/HOL/Auth/NS_Shared.ML Tue Sep 22 17:08:30 1998 +0200
+++ b/src/HOL/Auth/NS_Shared.ML Wed Sep 23 10:03:32 1998 +0200
@@ -236,8 +236,8 @@
by analz_spies_tac;
by (ALLGOALS
(asm_simp_tac
- (simpset() addsimps ([analz_insert_eq, analz_insert_freshK] @
- pushes @ split_ifs))));
+ (simpset() addsimps [analz_insert_eq, analz_insert_freshK] @
+ pushes @ split_ifs)));
(*Oops*)
by (blast_tac (claset() addDs [unique_session_keys]) 5);
(*NS3, replay sub-case*)
--- a/src/HOL/Auth/OtwayRees.ML Tue Sep 22 17:08:30 1998 +0200
+++ b/src/HOL/Auth/OtwayRees.ML Wed Sep 23 10:03:32 1998 +0200
@@ -289,7 +289,7 @@
by (ALLGOALS
(asm_simp_tac (simpset() addcongs [conj_cong]
addsimps [analz_insert_eq, analz_insert_freshK]
- addsimps (pushes@split_ifs))));
+ @ pushes @ split_ifs)));
(*Oops*)
by (blast_tac (claset() addSDs [unique_session_keys]) 4);
(*OR4*)
--- a/src/HOL/Auth/OtwayRees_AN.ML Tue Sep 22 17:08:30 1998 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.ML Wed Sep 23 10:03:32 1998 +0200
@@ -230,7 +230,7 @@
by (ALLGOALS
(asm_simp_tac (simpset() addcongs [conj_cong, if_weak_cong]
addsimps [analz_insert_eq, analz_insert_freshK]
- addsimps (pushes@split_ifs))));
+ @ pushes @ split_ifs)));
(*Oops*)
by (blast_tac (claset() addSDs [unique_session_keys]) 4);
(*OR4*)
--- a/src/HOL/Auth/OtwayRees_Bad.ML Tue Sep 22 17:08:30 1998 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.ML Wed Sep 23 10:03:32 1998 +0200
@@ -199,7 +199,7 @@
by (ALLGOALS
(asm_simp_tac (simpset() addcongs [conj_cong]
addsimps [analz_insert_eq, analz_insert_freshK]
- addsimps (pushes@split_ifs))));
+ @ pushes @ split_ifs)));
(*Oops*)
by (blast_tac (claset() addSDs [unique_session_keys]) 4);
(*OR4*)
--- a/src/HOL/Auth/Recur.ML Tue Sep 22 17:08:30 1998 +0200
+++ b/src/HOL/Auth/Recur.ML Wed Sep 23 10:03:32 1998 +0200
@@ -387,8 +387,7 @@
by analz_spies_tac;
by (ALLGOALS
(asm_simp_tac
- (simpset() addsimps (split_ifs @
- [analz_insert_eq, analz_insert_freshK]))));
+ (simpset() addsimps split_ifs @ [analz_insert_eq, analz_insert_freshK])));
(*RA4*)
by (spy_analz_tac 5);
(*RA2*)
--- a/src/HOL/Auth/Shared.ML Tue Sep 22 17:08:30 1998 +0200
+++ b/src/HOL/Auth/Shared.ML Wed Sep 23 10:03:32 1998 +0200
@@ -237,11 +237,11 @@
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);
+ 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 Tue Sep 22 17:08:30 1998 +0200
+++ b/src/HOL/Auth/TLS.ML Wed Sep 23 10:03:32 1998 +0200
@@ -178,7 +178,7 @@
ClientKeyExch_tac (i+6) THEN (*ClientKeyExch*)
ALLGOALS (asm_simp_tac
(simpset() addcongs [if_weak_cong]
- addsimps (split_ifs@pushes))) THEN
+ 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
@@ -343,7 +343,7 @@
by (etac tls.induct 1);
by (ALLGOALS
(asm_simp_tac (analz_image_keys_ss
- addsimps (certificate_def::keys_distinct))));
+ addsimps certificate_def::keys_distinct)));
(*Fake*)
by (spy_analz_tac 1);
qed_spec_mp "analz_image_priK";
@@ -375,9 +375,9 @@
by (REPEAT_FIRST (rtac analz_image_keys_lemma));
by (ALLGOALS (*4.5 seconds*)
(asm_simp_tac (analz_image_keys_ss
- addsimps (split_ifs@pushes)
- addsimps [range_sessionkeys_not_priK,
- analz_image_priK, certificate_def])));
+ addsimps split_ifs @ pushes @
+ [range_sessionkeys_not_priK,
+ analz_image_priK, certificate_def])));
by (ALLGOALS (asm_simp_tac (simpset() addsimps [insert_absorb])));
(*Fake*)
by (spy_analz_tac 1);
--- a/src/HOL/Auth/Yahalom.ML Tue Sep 22 17:08:30 1998 +0200
+++ b/src/HOL/Auth/Yahalom.ML Wed Sep 23 10:03:32 1998 +0200
@@ -190,8 +190,8 @@
by analz_spies_tac;
by (ALLGOALS
(asm_simp_tac
- (simpset() addsimps (split_ifs@pushes)
- addsimps [analz_insert_eq, analz_insert_freshK])));
+ (simpset() addsimps split_ifs @ pushes @
+ [analz_insert_eq, analz_insert_freshK])));
(*Oops*)
by (blast_tac (claset() addDs [unique_session_keys]) 3);
(*YM3*)
@@ -465,8 +465,8 @@
by analz_spies_tac;
by (ALLGOALS
(asm_simp_tac
- (simpset() addsimps (split_ifs@pushes)
- addsimps [analz_insert_eq, analz_insert_freshK])));
+ (simpset() addsimps split_ifs @ pushes @
+ [analz_insert_eq, analz_insert_freshK])));
(*Prove YM3 by showing that no NB can also be an NA*)
by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj]
addSEs [MPair_parts]
--- a/src/HOL/IMP/Expr.ML Tue Sep 22 17:08:30 1998 +0200
+++ b/src/HOL/IMP/Expr.ML Wed Sep 23 10:03:32 1998 +0200
@@ -32,14 +32,12 @@
Goal "!n. ((a,s) -a-> n) = (A a s = n)";
by (induct_tac "a" 1);
-by (ALLGOALS
- (fast_tac (claset() addSIs evala.intrs
- addSEs evala_elim_cases addss (simpset()))));
+by (auto_tac (claset() addSIs evala.intrs addSEs evala_elim_cases,
+ simpset()));
qed_spec_mp "aexp_iff";
Goal "!w. ((b,s) -b-> w) = (B b s = w)";
by (induct_tac "b" 1);
-by (ALLGOALS
- (fast_tac (claset()
- addss (simpset() addsimps (aexp_iff::evalb_simps)))));
+by (auto_tac (claset(),
+ simpset() addsimps aexp_iff::evalb_simps));
qed_spec_mp "bexp_iff";
--- a/src/HOL/Induct/FoldSet.ML Tue Sep 22 17:08:30 1998 +0200
+++ b/src/HOL/Induct/FoldSet.ML Wed Sep 23 10:03:32 1998 +0200
@@ -138,7 +138,7 @@
by (etac finite_induct 1);
by (Simp_tac 1);
by (asm_simp_tac
- (simpset() addsimps (f_ac @ [insert_absorb, Int_insert_left])) 1);
+ (simpset() addsimps f_ac @ [insert_absorb, Int_insert_left]) 1);
by (rtac impI 1);
by (stac f_commute 1 THEN rtac refl 1);
qed "fold_Un_Int";
--- a/src/HOL/Induct/SList.ML Tue Sep 22 17:08:30 1998 +0200
+++ b/src/HOL/Induct/SList.ML Wed Sep 23 10:03:32 1998 +0200
@@ -229,7 +229,7 @@
val sexp_ListA_I = A_subset_sexp RS list_subset_sexp RS subsetD;
val sexp_A_I = A_subset_sexp RS subsetD;
by (rtac (major RS list.induct) 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsimps ([sexp_A_I,sexp_ListA_I]@prems))));
+by (ALLGOALS(asm_simp_tac (simpset() addsimps [sexp_A_I,sexp_ListA_I]@prems)));
qed "List_rec_type";
(** Generalized map functionals **)
--- a/src/HOL/Real/PRat.ML Tue Sep 22 17:08:30 1998 +0200
+++ b/src/HOL/Real/PRat.ML Wed Sep 23 10:03:32 1998 +0200
@@ -177,15 +177,16 @@
Goal "(z::prat) + w = w + z";
by (res_inst_tac [("z","z")] eq_Abs_prat 1);
by (res_inst_tac [("z","w")] eq_Abs_prat 1);
-by (asm_simp_tac (simpset() addsimps ([prat_add] @ pnat_add_ac @ pnat_mult_ac)) 1);
+by (asm_simp_tac
+ (simpset() addsimps [prat_add] @ pnat_add_ac @ pnat_mult_ac) 1);
qed "prat_add_commute";
Goal "((z1::prat) + z2) + z3 = z1 + (z2 + z3)";
by (res_inst_tac [("z","z1")] eq_Abs_prat 1);
by (res_inst_tac [("z","z2")] eq_Abs_prat 1);
by (res_inst_tac [("z","z3")] eq_Abs_prat 1);
-by (asm_simp_tac (simpset() addsimps ([pnat_add_mult_distrib2,prat_add] @
- pnat_add_ac @ pnat_mult_ac)) 1);
+by (asm_simp_tac (simpset() addsimps [pnat_add_mult_distrib2,prat_add] @
+ pnat_add_ac @ pnat_mult_ac) 1);
qed "prat_add_assoc";
qed_goal "prat_add_left_commute" thy
@@ -225,7 +226,7 @@
Goal "(z::prat) * w = w * z";
by (res_inst_tac [("z","z")] eq_Abs_prat 1);
by (res_inst_tac [("z","w")] eq_Abs_prat 1);
-by (asm_simp_tac (simpset() addsimps (pnat_mult_ac @ [prat_mult])) 1);
+by (asm_simp_tac (simpset() addsimps pnat_mult_ac @ [prat_mult]) 1);
qed "prat_mult_commute";
Goal "((z1::prat) * z2) * z3 = z1 * (z2 * z3)";
@@ -333,8 +334,8 @@
by (res_inst_tac [("z","z2")] eq_Abs_prat 1);
by (res_inst_tac [("z","w")] eq_Abs_prat 1);
by (asm_simp_tac
- (simpset() addsimps ([pnat_add_mult_distrib2, prat_add, prat_mult] @
- pnat_add_ac @ pnat_mult_ac)) 1);
+ (simpset() addsimps [pnat_add_mult_distrib2, prat_add, prat_mult] @
+ pnat_add_ac @ pnat_mult_ac) 1);
qed "prat_add_mult_distrib";
val prat_mult_commute'= read_instantiate [("z","w")] prat_mult_commute;
--- a/src/HOL/Real/Real.ML Tue Sep 22 17:08:30 1998 +0200
+++ b/src/HOL/Real/Real.ML Wed Sep 23 10:03:32 1998 +0200
@@ -176,7 +176,7 @@
Goal "(z::real) + w = w + z";
by (res_inst_tac [("z","z")] eq_Abs_real 1);
by (res_inst_tac [("z","w")] eq_Abs_real 1);
-by (asm_simp_tac (simpset() addsimps (preal_add_ac @ [real_add])) 1);
+by (asm_simp_tac (simpset() addsimps preal_add_ac @ [real_add]) 1);
qed "real_add_commute";
Goal "((z1::real) + z2) + z3 = z1 + (z2 + z3)";
@@ -303,15 +303,16 @@
Goal "(z::real) * w = w * z";
by (res_inst_tac [("z","z")] eq_Abs_real 1);
by (res_inst_tac [("z","w")] eq_Abs_real 1);
-by (asm_simp_tac (simpset() addsimps ([real_mult] @ preal_add_ac @ preal_mult_ac)) 1);
+by (asm_simp_tac
+ (simpset() addsimps [real_mult] @ preal_add_ac @ preal_mult_ac) 1);
qed "real_mult_commute";
Goal "((z1::real) * z2) * z3 = z1 * (z2 * z3)";
by (res_inst_tac [("z","z1")] eq_Abs_real 1);
by (res_inst_tac [("z","z2")] eq_Abs_real 1);
by (res_inst_tac [("z","z3")] eq_Abs_real 1);
-by (asm_simp_tac (simpset() addsimps ([preal_add_mult_distrib2,real_mult] @
- preal_add_ac @ preal_mult_ac)) 1);
+by (asm_simp_tac (simpset() addsimps [preal_add_mult_distrib2,real_mult] @
+ preal_add_ac @ preal_mult_ac) 1);
qed "real_mult_assoc";
qed_goal "real_mult_left_commute" thy
@@ -392,8 +393,8 @@
by (res_inst_tac [("z","z2")] eq_Abs_real 1);
by (res_inst_tac [("z","w")] eq_Abs_real 1);
by (asm_simp_tac
- (simpset() addsimps ([preal_add_mult_distrib2, real_add, real_mult] @
- preal_add_ac @ preal_mult_ac)) 1);
+ (simpset() addsimps [preal_add_mult_distrib2, real_add, real_mult] @
+ preal_add_ac @ preal_mult_ac) 1);
qed "real_add_mult_distrib";
val real_mult_commute'= read_instantiate [("z","w")] real_mult_commute;