src/HOL/Arith.ML
changeset 5537 c2bd39a2c0ee
parent 5497 497215d66441
child 5598 6b8dee1a6ebb
     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