deleted needless parentheses
authorpaulson
Wed Sep 23 10:12:01 1998 +0200 (1998-09-23)
changeset 5537c2bd39a2c0ee
parent 5536 130f3d891fb2
child 5538 c55bf0487abe
deleted needless parentheses
src/HOL/Arith.ML
src/HOL/Divides.ML
src/HOL/Finite.ML
src/HOL/List.ML
src/HOL/ex/Fib.ML
     1.1 --- a/src/HOL/Arith.ML	Wed Sep 23 10:11:18 1998 +0200
     1.2 +++ b/src/HOL/Arith.ML	Wed Sep 23 10:12:01 1998 +0200
     1.3 @@ -202,8 +202,8 @@
     1.4  Goal "!!k:: nat. [| k<l;  m+l = k+n |] ==> m<n";
     1.5  by (auto_tac (claset(),
     1.6  	      simpset() delsimps [add_Suc_right]
     1.7 -	                addsimps ([less_iff_Suc_add,
     1.8 -				   add_Suc_right RS sym] @ add_ac)));
     1.9 +	                addsimps [less_iff_Suc_add,
    1.10 +				  add_Suc_right RS sym] @ add_ac));
    1.11  qed "less_add_eq_less";
    1.12  
    1.13  
    1.14 @@ -378,7 +378,7 @@
    1.15  Goal "i<n ==> n - Suc i < n - i";
    1.16  by (exhaust_tac "n" 1);
    1.17  by (auto_tac (claset(),
    1.18 -	      simpset() addsimps ([Suc_diff_le]@le_simps)));
    1.19 +	      simpset() addsimps [Suc_diff_le]@le_simps));
    1.20  qed "diff_Suc_less_diff";
    1.21  
    1.22  Goal "m - n <= Suc m - n";
    1.23 @@ -471,7 +471,7 @@
    1.24  
    1.25  Goal "(m+k) - (n+k) = m - (n::nat)";
    1.26  val add_commute_k = read_instantiate [("n","k")] add_commute;
    1.27 -by (asm_simp_tac (simpset() addsimps ([add_commute_k])) 1);
    1.28 +by (asm_simp_tac (simpset() addsimps [add_commute_k]) 1);
    1.29  qed "diff_cancel2";
    1.30  Addsimps [diff_cancel2];
    1.31  
     2.1 --- a/src/HOL/Divides.ML	Wed Sep 23 10:11:18 1998 +0200
     2.2 +++ b/src/HOL/Divides.ML	Wed Sep 23 10:12:01 1998 +0200
     2.3 @@ -61,7 +61,7 @@
     2.4  
     2.5  Goal "!!n. 0<n ==> (m + k*n) mod n = m mod n";
     2.6  by (induct_tac "k" 1);
     2.7 -by (ALLGOALS (asm_simp_tac (simpset() addsimps (add_ac @ [mod_add_self1]))));
     2.8 +by (ALLGOALS (asm_simp_tac (simpset() addsimps add_ac @ [mod_add_self1])));
     2.9  qed "mod_mult_self1";
    2.10  
    2.11  Goal "0<n ==> (m + n*k) mod n = m mod n";
    2.12 @@ -126,9 +126,8 @@
    2.13  by (res_inst_tac [("n","m")] less_induct 1);
    2.14  by (stac mod_if 1);
    2.15  by (ALLGOALS (asm_simp_tac 
    2.16 -	      (simpset() addsimps ([add_assoc] @
    2.17 -				   [div_less, div_geq,
    2.18 -				    add_diff_inverse, diff_less]))));
    2.19 +	      (simpset() addsimps [add_assoc, div_less, div_geq,
    2.20 +				   add_diff_inverse, diff_less])));
    2.21  qed "mod_div_equality";
    2.22  
    2.23  (* a simple rearrangement of mod_div_equality: *)
    2.24 @@ -161,7 +160,7 @@
    2.25  
    2.26  Goal "!!n. 0<n ==> (m + k*n) div n = k + m div n";
    2.27  by (induct_tac "k" 1);
    2.28 -by (ALLGOALS (asm_simp_tac (simpset() addsimps (add_ac @ [div_add_self1]))));
    2.29 +by (ALLGOALS (asm_simp_tac (simpset() addsimps add_ac @ [div_add_self1])));
    2.30  qed "div_mult_self1";
    2.31  
    2.32  Goal "0<n ==> (m + n*k) div n = k + m div n";
     3.1 --- a/src/HOL/Finite.ML	Wed Sep 23 10:11:18 1998 +0200
     3.2 +++ b/src/HOL/Finite.ML	Wed Sep 23 10:12:01 1998 +0200
     3.3 @@ -93,7 +93,7 @@
     3.4  by (rtac (major RS finite_induct) 1);
     3.5  by (stac Diff_insert 2);
     3.6  by (ALLGOALS (asm_simp_tac
     3.7 -                (simpset() addsimps (prems@[Diff_subset RS finite_subset]))));
     3.8 +                (simpset() addsimps prems@[Diff_subset RS finite_subset])));
     3.9  val lemma = result();
    3.10  
    3.11  val prems = Goal 
     4.1 --- a/src/HOL/List.ML	Wed Sep 23 10:11:18 1998 +0200
     4.2 +++ b/src/HOL/List.ML	Wed Sep 23 10:12:01 1998 +0200
     4.3 @@ -900,7 +900,7 @@
     4.4  Goal "i+k < j --> [i..j(] ! k = i+k";
     4.5  by(induct_tac "j" 1);
     4.6   by(Simp_tac 1);
     4.7 -by(asm_simp_tac (simpset() addsimps ([nth_append,less_diff_conv]@add_ac)
     4.8 +by(asm_simp_tac (simpset() addsimps [nth_append,less_diff_conv]@add_ac
     4.9                             addSolver cut_trans_tac) 1);
    4.10  br conjI 1;
    4.11   by(Clarify_tac 1);
     5.1 --- a/src/HOL/ex/Fib.ML	Wed Sep 23 10:11:18 1998 +0200
     5.2 +++ b/src/HOL/ex/Fib.ML	Wed Sep 23 10:12:01 1998 +0200
     5.3 @@ -65,9 +65,9 @@
     5.4  				       mod_less, mod_Suc])));
     5.5  by (ALLGOALS
     5.6      (asm_full_simp_tac
     5.7 -     (simpset() addsimps ([] @ add_ac @ mult_ac @
     5.8 +     (simpset() addsimps add_ac @ mult_ac @
     5.9  			 [fib_Suc_Suc, add_mult_distrib, add_mult_distrib2, 
    5.10 -			  mod_less, mod_Suc]))));
    5.11 +			  mod_less, mod_Suc])));
    5.12  qed "fib_Cassini";
    5.13  
    5.14