# HG changeset patch # User paulson # Date 906537812 -7200 # Node ID 678999604ee98266d8c9be2f675f9bb6c4860553 # Parent c2cd79a6645f158f399abdf2a1a3af16842e03e2 deleted needless parentheses diff -r c2cd79a6645f -r 678999604ee9 src/HOL/Auth/Kerberos_BAN.ML --- 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*) diff -r c2cd79a6645f -r 678999604ee9 src/HOL/Auth/NS_Shared.ML --- 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*) diff -r c2cd79a6645f -r 678999604ee9 src/HOL/Auth/OtwayRees.ML --- 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*) diff -r c2cd79a6645f -r 678999604ee9 src/HOL/Auth/OtwayRees_AN.ML --- 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*) diff -r c2cd79a6645f -r 678999604ee9 src/HOL/Auth/OtwayRees_Bad.ML --- 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*) diff -r c2cd79a6645f -r 678999604ee9 src/HOL/Auth/Recur.ML --- 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*) diff -r c2cd79a6645f -r 678999604ee9 src/HOL/Auth/Shared.ML --- 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) ==> \ diff -r c2cd79a6645f -r 678999604ee9 src/HOL/Auth/TLS.ML --- 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); diff -r c2cd79a6645f -r 678999604ee9 src/HOL/Auth/Yahalom.ML --- 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] diff -r c2cd79a6645f -r 678999604ee9 src/HOL/IMP/Expr.ML --- 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"; diff -r c2cd79a6645f -r 678999604ee9 src/HOL/Induct/FoldSet.ML --- 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"; diff -r c2cd79a6645f -r 678999604ee9 src/HOL/Induct/SList.ML --- 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 **) diff -r c2cd79a6645f -r 678999604ee9 src/HOL/Real/PRat.ML --- 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; diff -r c2cd79a6645f -r 678999604ee9 src/HOL/Real/Real.ML --- 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;