deleted needless parentheses
authorpaulson
Wed Sep 23 10:03:32 1998 +0200 (1998-09-23)
changeset 5535678999604ee9
parent 5534 c2cd79a6645f
child 5536 130f3d891fb2
deleted needless parentheses
src/HOL/Auth/Kerberos_BAN.ML
src/HOL/Auth/NS_Shared.ML
src/HOL/Auth/OtwayRees.ML
src/HOL/Auth/OtwayRees_AN.ML
src/HOL/Auth/OtwayRees_Bad.ML
src/HOL/Auth/Recur.ML
src/HOL/Auth/Shared.ML
src/HOL/Auth/TLS.ML
src/HOL/Auth/Yahalom.ML
src/HOL/IMP/Expr.ML
src/HOL/Induct/FoldSet.ML
src/HOL/Induct/SList.ML
src/HOL/Real/PRat.ML
src/HOL/Real/Real.ML
     1.1 --- a/src/HOL/Auth/Kerberos_BAN.ML	Tue Sep 22 17:08:30 1998 +0200
     1.2 +++ b/src/HOL/Auth/Kerberos_BAN.ML	Wed Sep 23 10:03:32 1998 +0200
     1.3 @@ -240,8 +240,8 @@
     1.4  by (etac kerberos_ban.induct 1);
     1.5  by analz_spies_tac;
     1.6  by (ALLGOALS
     1.7 -    (asm_simp_tac (simpset() addsimps ([analz_insert_eq, analz_insert_freshK]
     1.8 -				       @ pushes))));
     1.9 +    (asm_simp_tac (simpset() addsimps [analz_insert_eq, analz_insert_freshK]
    1.10 +				      @ pushes)));
    1.11  (*Oops*)
    1.12  by (blast_tac (claset() addDs [unique_session_keys] addIs [less_SucI]) 4);
    1.13  (*Kb2*)
     2.1 --- a/src/HOL/Auth/NS_Shared.ML	Tue Sep 22 17:08:30 1998 +0200
     2.2 +++ b/src/HOL/Auth/NS_Shared.ML	Wed Sep 23 10:03:32 1998 +0200
     2.3 @@ -236,8 +236,8 @@
     2.4  by analz_spies_tac;
     2.5  by (ALLGOALS 
     2.6      (asm_simp_tac 
     2.7 -     (simpset() addsimps ([analz_insert_eq, analz_insert_freshK] @ 
     2.8 -			  pushes @ split_ifs))));
     2.9 +     (simpset() addsimps [analz_insert_eq, analz_insert_freshK] @ 
    2.10 +			 pushes @ split_ifs)));
    2.11  (*Oops*)
    2.12  by (blast_tac (claset() addDs [unique_session_keys]) 5);
    2.13  (*NS3, replay sub-case*) 
     3.1 --- a/src/HOL/Auth/OtwayRees.ML	Tue Sep 22 17:08:30 1998 +0200
     3.2 +++ b/src/HOL/Auth/OtwayRees.ML	Wed Sep 23 10:03:32 1998 +0200
     3.3 @@ -289,7 +289,7 @@
     3.4  by (ALLGOALS
     3.5      (asm_simp_tac (simpset() addcongs [conj_cong] 
     3.6                               addsimps [analz_insert_eq, analz_insert_freshK]
     3.7 -                             addsimps (pushes@split_ifs))));
     3.8 +                                      @ pushes @ split_ifs)));
     3.9  (*Oops*)
    3.10  by (blast_tac (claset() addSDs [unique_session_keys]) 4);
    3.11  (*OR4*) 
     4.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Tue Sep 22 17:08:30 1998 +0200
     4.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Wed Sep 23 10:03:32 1998 +0200
     4.3 @@ -230,7 +230,7 @@
     4.4  by (ALLGOALS
     4.5      (asm_simp_tac (simpset() addcongs [conj_cong, if_weak_cong] 
     4.6                               addsimps [analz_insert_eq, analz_insert_freshK]
     4.7 -                             addsimps (pushes@split_ifs))));
     4.8 +                                      @ pushes @ split_ifs)));
     4.9  (*Oops*)
    4.10  by (blast_tac (claset() addSDs [unique_session_keys]) 4);
    4.11  (*OR4*) 
     5.1 --- a/src/HOL/Auth/OtwayRees_Bad.ML	Tue Sep 22 17:08:30 1998 +0200
     5.2 +++ b/src/HOL/Auth/OtwayRees_Bad.ML	Wed Sep 23 10:03:32 1998 +0200
     5.3 @@ -199,7 +199,7 @@
     5.4  by (ALLGOALS
     5.5      (asm_simp_tac (simpset() addcongs [conj_cong] 
     5.6                               addsimps [analz_insert_eq, analz_insert_freshK]
     5.7 -                             addsimps (pushes@split_ifs))));
     5.8 +                                      @ pushes @ split_ifs)));
     5.9  (*Oops*)
    5.10  by (blast_tac (claset() addSDs [unique_session_keys]) 4);
    5.11  (*OR4*) 
     6.1 --- a/src/HOL/Auth/Recur.ML	Tue Sep 22 17:08:30 1998 +0200
     6.2 +++ b/src/HOL/Auth/Recur.ML	Wed Sep 23 10:03:32 1998 +0200
     6.3 @@ -387,8 +387,7 @@
     6.4  by analz_spies_tac;
     6.5  by (ALLGOALS
     6.6      (asm_simp_tac
     6.7 -     (simpset() addsimps (split_ifs @
     6.8 -			 [analz_insert_eq, analz_insert_freshK]))));
     6.9 +     (simpset() addsimps split_ifs @ [analz_insert_eq, analz_insert_freshK])));
    6.10  (*RA4*)
    6.11  by (spy_analz_tac 5);
    6.12  (*RA2*)
     7.1 --- a/src/HOL/Auth/Shared.ML	Tue Sep 22 17:08:30 1998 +0200
     7.2 +++ b/src/HOL/Auth/Shared.ML	Wed Sep 23 10:03:32 1998 +0200
     7.3 @@ -237,11 +237,11 @@
     7.4       simpset() addcongs [if_weak_cong]
     7.5  	      delsimps [image_insert, image_Un]
     7.6                delsimps [imp_disjL]    (*reduces blow-up*)
     7.7 -              addsimps ([image_insert RS sym, image_Un RS sym,
     7.8 -                         analz_insert_eq, impOfSubs (Un_upper2 RS analz_mono),
     7.9 -                         insert_Key_singleton, subset_Compl_range,
    7.10 -                         Key_not_used, insert_Key_image, Un_assoc RS sym]
    7.11 -                        @disj_comms);
    7.12 +              addsimps [image_insert RS sym, image_Un RS sym,
    7.13 +			analz_insert_eq, impOfSubs (Un_upper2 RS analz_mono),
    7.14 +			insert_Key_singleton, subset_Compl_range,
    7.15 +			Key_not_used, insert_Key_image, Un_assoc RS sym]
    7.16 +                       @disj_comms;
    7.17  
    7.18  (*Lemma for the trivial direction of the if-and-only-if*)
    7.19  Goal "(Key K : analz (Key``nE Un H)) --> (K : nE | Key K : analz H)  ==> \
     8.1 --- a/src/HOL/Auth/TLS.ML	Tue Sep 22 17:08:30 1998 +0200
     8.2 +++ b/src/HOL/Auth/TLS.ML	Wed Sep 23 10:03:32 1998 +0200
     8.3 @@ -178,7 +178,7 @@
     8.4      ClientKeyExch_tac  (i+6)  THEN	(*ClientKeyExch*)
     8.5      ALLGOALS (asm_simp_tac 
     8.6                (simpset() addcongs [if_weak_cong]
     8.7 -                         addsimps (split_ifs@pushes)))  THEN
     8.8 +                         addsimps split_ifs @ pushes))  THEN
     8.9      (*Remove instances of pubK B:  the Spy already knows all public keys.
    8.10        Combining the two simplifier calls makes them run extremely slowly.*)
    8.11      ALLGOALS (asm_simp_tac 
    8.12 @@ -343,7 +343,7 @@
    8.13  by (etac tls.induct 1);
    8.14  by (ALLGOALS
    8.15      (asm_simp_tac (analz_image_keys_ss
    8.16 -		   addsimps (certificate_def::keys_distinct))));
    8.17 +		   addsimps certificate_def::keys_distinct)));
    8.18  (*Fake*) 
    8.19  by (spy_analz_tac 1);
    8.20  qed_spec_mp "analz_image_priK";
    8.21 @@ -375,9 +375,9 @@
    8.22  by (REPEAT_FIRST (rtac analz_image_keys_lemma));
    8.23  by (ALLGOALS    (*4.5 seconds*)
    8.24      (asm_simp_tac (analz_image_keys_ss 
    8.25 -		   addsimps (split_ifs@pushes)
    8.26 -		   addsimps [range_sessionkeys_not_priK, 
    8.27 -                             analz_image_priK, certificate_def])));
    8.28 +		   addsimps split_ifs @ pushes @
    8.29 +		            [range_sessionkeys_not_priK, 
    8.30 +			     analz_image_priK, certificate_def])));
    8.31  by (ALLGOALS (asm_simp_tac (simpset() addsimps [insert_absorb])));
    8.32  (*Fake*) 
    8.33  by (spy_analz_tac 1);
     9.1 --- a/src/HOL/Auth/Yahalom.ML	Tue Sep 22 17:08:30 1998 +0200
     9.2 +++ b/src/HOL/Auth/Yahalom.ML	Wed Sep 23 10:03:32 1998 +0200
     9.3 @@ -190,8 +190,8 @@
     9.4  by analz_spies_tac;
     9.5  by (ALLGOALS
     9.6      (asm_simp_tac 
     9.7 -     (simpset() addsimps (split_ifs@pushes)
     9.8 -	        addsimps [analz_insert_eq, analz_insert_freshK])));
     9.9 +     (simpset() addsimps split_ifs @ pushes @
    9.10 +                         [analz_insert_eq, analz_insert_freshK])));
    9.11  (*Oops*)
    9.12  by (blast_tac (claset() addDs [unique_session_keys]) 3);
    9.13  (*YM3*)
    9.14 @@ -465,8 +465,8 @@
    9.15  by analz_spies_tac;
    9.16  by (ALLGOALS
    9.17      (asm_simp_tac 
    9.18 -     (simpset() addsimps (split_ifs@pushes)
    9.19 -	        addsimps [analz_insert_eq, analz_insert_freshK])));
    9.20 +     (simpset() addsimps split_ifs @ pushes @
    9.21 +	                 [analz_insert_eq, analz_insert_freshK])));
    9.22  (*Prove YM3 by showing that no NB can also be an NA*)
    9.23  by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj]
    9.24  	                addSEs [MPair_parts]
    10.1 --- a/src/HOL/IMP/Expr.ML	Tue Sep 22 17:08:30 1998 +0200
    10.2 +++ b/src/HOL/IMP/Expr.ML	Wed Sep 23 10:03:32 1998 +0200
    10.3 @@ -32,14 +32,12 @@
    10.4  
    10.5  Goal "!n. ((a,s) -a-> n) = (A a s = n)";
    10.6  by (induct_tac "a" 1);
    10.7 -by (ALLGOALS 
    10.8 -    (fast_tac (claset() addSIs evala.intrs
    10.9 -	                addSEs evala_elim_cases addss (simpset()))));
   10.10 +by (auto_tac (claset() addSIs evala.intrs addSEs evala_elim_cases,
   10.11 +	      simpset()));
   10.12  qed_spec_mp "aexp_iff";
   10.13  
   10.14  Goal "!w. ((b,s) -b-> w) = (B b s = w)";
   10.15  by (induct_tac "b" 1);
   10.16 -by (ALLGOALS 
   10.17 -    (fast_tac (claset() 
   10.18 -	       addss (simpset() addsimps (aexp_iff::evalb_simps)))));
   10.19 +by (auto_tac (claset(), 
   10.20 +	      simpset() addsimps aexp_iff::evalb_simps));
   10.21  qed_spec_mp "bexp_iff";
    11.1 --- a/src/HOL/Induct/FoldSet.ML	Tue Sep 22 17:08:30 1998 +0200
    11.2 +++ b/src/HOL/Induct/FoldSet.ML	Wed Sep 23 10:03:32 1998 +0200
    11.3 @@ -138,7 +138,7 @@
    11.4  by (etac finite_induct 1);
    11.5  by (Simp_tac 1);
    11.6  by (asm_simp_tac
    11.7 -    (simpset() addsimps (f_ac @ [insert_absorb, Int_insert_left])) 1);
    11.8 +    (simpset() addsimps f_ac @ [insert_absorb, Int_insert_left]) 1);
    11.9  by (rtac impI 1);
   11.10  by (stac f_commute 1 THEN rtac refl 1);
   11.11  qed "fold_Un_Int";
    12.1 --- a/src/HOL/Induct/SList.ML	Tue Sep 22 17:08:30 1998 +0200
    12.2 +++ b/src/HOL/Induct/SList.ML	Wed Sep 23 10:03:32 1998 +0200
    12.3 @@ -229,7 +229,7 @@
    12.4  val sexp_ListA_I = A_subset_sexp RS list_subset_sexp RS subsetD;
    12.5  val sexp_A_I = A_subset_sexp RS subsetD;
    12.6  by (rtac (major RS list.induct) 1);
    12.7 -by (ALLGOALS(asm_simp_tac (simpset() addsimps ([sexp_A_I,sexp_ListA_I]@prems))));
    12.8 +by (ALLGOALS(asm_simp_tac (simpset() addsimps [sexp_A_I,sexp_ListA_I]@prems)));
    12.9  qed "List_rec_type";
   12.10  
   12.11  (** Generalized map functionals **)
    13.1 --- a/src/HOL/Real/PRat.ML	Tue Sep 22 17:08:30 1998 +0200
    13.2 +++ b/src/HOL/Real/PRat.ML	Wed Sep 23 10:03:32 1998 +0200
    13.3 @@ -177,15 +177,16 @@
    13.4  Goal "(z::prat) + w = w + z";
    13.5  by (res_inst_tac [("z","z")] eq_Abs_prat 1);
    13.6  by (res_inst_tac [("z","w")] eq_Abs_prat 1);
    13.7 -by (asm_simp_tac (simpset() addsimps ([prat_add] @ pnat_add_ac @ pnat_mult_ac)) 1);
    13.8 +by (asm_simp_tac
    13.9 +    (simpset() addsimps [prat_add] @ pnat_add_ac @ pnat_mult_ac) 1);
   13.10  qed "prat_add_commute";
   13.11  
   13.12  Goal "((z1::prat) + z2) + z3 = z1 + (z2 + z3)";
   13.13  by (res_inst_tac [("z","z1")] eq_Abs_prat 1);
   13.14  by (res_inst_tac [("z","z2")] eq_Abs_prat 1);
   13.15  by (res_inst_tac [("z","z3")] eq_Abs_prat 1);
   13.16 -by (asm_simp_tac (simpset() addsimps ([pnat_add_mult_distrib2,prat_add] @ 
   13.17 -                                     pnat_add_ac @ pnat_mult_ac)) 1);
   13.18 +by (asm_simp_tac (simpset() addsimps [pnat_add_mult_distrib2,prat_add] @ 
   13.19 +                                     pnat_add_ac @ pnat_mult_ac) 1);
   13.20  qed "prat_add_assoc";
   13.21  
   13.22  qed_goal "prat_add_left_commute" thy
   13.23 @@ -225,7 +226,7 @@
   13.24  Goal "(z::prat) * w = w * z";
   13.25  by (res_inst_tac [("z","z")] eq_Abs_prat 1);
   13.26  by (res_inst_tac [("z","w")] eq_Abs_prat 1);
   13.27 -by (asm_simp_tac (simpset() addsimps (pnat_mult_ac @ [prat_mult])) 1);
   13.28 +by (asm_simp_tac (simpset() addsimps pnat_mult_ac @ [prat_mult]) 1);
   13.29  qed "prat_mult_commute";
   13.30  
   13.31  Goal "((z1::prat) * z2) * z3 = z1 * (z2 * z3)";
   13.32 @@ -333,8 +334,8 @@
   13.33  by (res_inst_tac [("z","z2")] eq_Abs_prat 1);
   13.34  by (res_inst_tac [("z","w")] eq_Abs_prat 1);
   13.35  by (asm_simp_tac 
   13.36 -    (simpset() addsimps ([pnat_add_mult_distrib2, prat_add, prat_mult] @ 
   13.37 -                        pnat_add_ac @ pnat_mult_ac)) 1);
   13.38 +    (simpset() addsimps [pnat_add_mult_distrib2, prat_add, prat_mult] @ 
   13.39 +                        pnat_add_ac @ pnat_mult_ac) 1);
   13.40  qed "prat_add_mult_distrib";
   13.41  
   13.42  val prat_mult_commute'= read_instantiate [("z","w")] prat_mult_commute;
    14.1 --- a/src/HOL/Real/Real.ML	Tue Sep 22 17:08:30 1998 +0200
    14.2 +++ b/src/HOL/Real/Real.ML	Wed Sep 23 10:03:32 1998 +0200
    14.3 @@ -176,7 +176,7 @@
    14.4  Goal "(z::real) + w = w + z";
    14.5  by (res_inst_tac [("z","z")] eq_Abs_real 1);
    14.6  by (res_inst_tac [("z","w")] eq_Abs_real 1);
    14.7 -by (asm_simp_tac (simpset() addsimps (preal_add_ac @ [real_add])) 1);
    14.8 +by (asm_simp_tac (simpset() addsimps preal_add_ac @ [real_add]) 1);
    14.9  qed "real_add_commute";
   14.10  
   14.11  Goal "((z1::real) + z2) + z3 = z1 + (z2 + z3)";
   14.12 @@ -303,15 +303,16 @@
   14.13  Goal "(z::real) * w = w * z";
   14.14  by (res_inst_tac [("z","z")] eq_Abs_real 1);
   14.15  by (res_inst_tac [("z","w")] eq_Abs_real 1);
   14.16 -by (asm_simp_tac (simpset() addsimps ([real_mult] @ preal_add_ac @ preal_mult_ac)) 1);
   14.17 +by (asm_simp_tac
   14.18 +    (simpset() addsimps [real_mult] @ preal_add_ac @ preal_mult_ac) 1);
   14.19  qed "real_mult_commute";
   14.20  
   14.21  Goal "((z1::real) * z2) * z3 = z1 * (z2 * z3)";
   14.22  by (res_inst_tac [("z","z1")] eq_Abs_real 1);
   14.23  by (res_inst_tac [("z","z2")] eq_Abs_real 1);
   14.24  by (res_inst_tac [("z","z3")] eq_Abs_real 1);
   14.25 -by (asm_simp_tac (simpset() addsimps ([preal_add_mult_distrib2,real_mult] @ 
   14.26 -                                     preal_add_ac @ preal_mult_ac)) 1);
   14.27 +by (asm_simp_tac (simpset() addsimps [preal_add_mult_distrib2,real_mult] @ 
   14.28 +                                     preal_add_ac @ preal_mult_ac) 1);
   14.29  qed "real_mult_assoc";
   14.30  
   14.31  qed_goal "real_mult_left_commute" thy
   14.32 @@ -392,8 +393,8 @@
   14.33  by (res_inst_tac [("z","z2")] eq_Abs_real 1);
   14.34  by (res_inst_tac [("z","w")] eq_Abs_real 1);
   14.35  by (asm_simp_tac 
   14.36 -    (simpset() addsimps ([preal_add_mult_distrib2, real_add, real_mult] @ 
   14.37 -                        preal_add_ac @ preal_mult_ac)) 1);
   14.38 +    (simpset() addsimps [preal_add_mult_distrib2, real_add, real_mult] @ 
   14.39 +                        preal_add_ac @ preal_mult_ac) 1);
   14.40  qed "real_add_mult_distrib";
   14.41  
   14.42  val real_mult_commute'= read_instantiate [("z","w")] real_mult_commute;