# HG changeset patch
# User paulson
# Date 906538321 -7200
# Node ID c2bd39a2c0eec341d6d87b6c95d38467ba83d18f
# Parent  130f3d891fb258f044ad4fdd1e7a1dd117cab916
deleted needless parentheses

diff -r 130f3d891fb2 -r c2bd39a2c0ee src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Wed Sep 23 10:11:18 1998 +0200
+++ b/src/HOL/Arith.ML	Wed Sep 23 10:12:01 1998 +0200
@@ -202,8 +202,8 @@
 Goal "!!k:: nat. [| k<l;  m+l = k+n |] ==> m<n";
 by (auto_tac (claset(),
 	      simpset() delsimps [add_Suc_right]
-	                addsimps ([less_iff_Suc_add,
-				   add_Suc_right RS sym] @ add_ac)));
+	                addsimps [less_iff_Suc_add,
+				  add_Suc_right RS sym] @ add_ac));
 qed "less_add_eq_less";
 
 
@@ -378,7 +378,7 @@
 Goal "i<n ==> n - Suc i < n - i";
 by (exhaust_tac "n" 1);
 by (auto_tac (claset(),
-	      simpset() addsimps ([Suc_diff_le]@le_simps)));
+	      simpset() addsimps [Suc_diff_le]@le_simps));
 qed "diff_Suc_less_diff";
 
 Goal "m - n <= Suc m - n";
@@ -471,7 +471,7 @@
 
 Goal "(m+k) - (n+k) = m - (n::nat)";
 val add_commute_k = read_instantiate [("n","k")] add_commute;
-by (asm_simp_tac (simpset() addsimps ([add_commute_k])) 1);
+by (asm_simp_tac (simpset() addsimps [add_commute_k]) 1);
 qed "diff_cancel2";
 Addsimps [diff_cancel2];
 
diff -r 130f3d891fb2 -r c2bd39a2c0ee src/HOL/Divides.ML
--- a/src/HOL/Divides.ML	Wed Sep 23 10:11:18 1998 +0200
+++ b/src/HOL/Divides.ML	Wed Sep 23 10:12:01 1998 +0200
@@ -61,7 +61,7 @@
 
 Goal "!!n. 0<n ==> (m + k*n) mod n = m mod n";
 by (induct_tac "k" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps (add_ac @ [mod_add_self1]))));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps add_ac @ [mod_add_self1])));
 qed "mod_mult_self1";
 
 Goal "0<n ==> (m + n*k) mod n = m mod n";
@@ -126,9 +126,8 @@
 by (res_inst_tac [("n","m")] less_induct 1);
 by (stac mod_if 1);
 by (ALLGOALS (asm_simp_tac 
-	      (simpset() addsimps ([add_assoc] @
-				   [div_less, div_geq,
-				    add_diff_inverse, diff_less]))));
+	      (simpset() addsimps [add_assoc, div_less, div_geq,
+				   add_diff_inverse, diff_less])));
 qed "mod_div_equality";
 
 (* a simple rearrangement of mod_div_equality: *)
@@ -161,7 +160,7 @@
 
 Goal "!!n. 0<n ==> (m + k*n) div n = k + m div n";
 by (induct_tac "k" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps (add_ac @ [div_add_self1]))));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps add_ac @ [div_add_self1])));
 qed "div_mult_self1";
 
 Goal "0<n ==> (m + n*k) div n = k + m div n";
diff -r 130f3d891fb2 -r c2bd39a2c0ee src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Wed Sep 23 10:11:18 1998 +0200
+++ b/src/HOL/Finite.ML	Wed Sep 23 10:12:01 1998 +0200
@@ -93,7 +93,7 @@
 by (rtac (major RS finite_induct) 1);
 by (stac Diff_insert 2);
 by (ALLGOALS (asm_simp_tac
-                (simpset() addsimps (prems@[Diff_subset RS finite_subset]))));
+                (simpset() addsimps prems@[Diff_subset RS finite_subset])));
 val lemma = result();
 
 val prems = Goal 
diff -r 130f3d891fb2 -r c2bd39a2c0ee src/HOL/List.ML
--- a/src/HOL/List.ML	Wed Sep 23 10:11:18 1998 +0200
+++ b/src/HOL/List.ML	Wed Sep 23 10:12:01 1998 +0200
@@ -900,7 +900,7 @@
 Goal "i+k < j --> [i..j(] ! k = i+k";
 by(induct_tac "j" 1);
  by(Simp_tac 1);
-by(asm_simp_tac (simpset() addsimps ([nth_append,less_diff_conv]@add_ac)
+by(asm_simp_tac (simpset() addsimps [nth_append,less_diff_conv]@add_ac
                            addSolver cut_trans_tac) 1);
 br conjI 1;
  by(Clarify_tac 1);
diff -r 130f3d891fb2 -r c2bd39a2c0ee src/HOL/ex/Fib.ML
--- a/src/HOL/ex/Fib.ML	Wed Sep 23 10:11:18 1998 +0200
+++ b/src/HOL/ex/Fib.ML	Wed Sep 23 10:12:01 1998 +0200
@@ -65,9 +65,9 @@
 				       mod_less, mod_Suc])));
 by (ALLGOALS
     (asm_full_simp_tac
-     (simpset() addsimps ([] @ add_ac @ mult_ac @
+     (simpset() addsimps add_ac @ mult_ac @
 			 [fib_Suc_Suc, add_mult_distrib, add_mult_distrib2, 
-			  mod_less, mod_Suc]))));
+			  mod_less, mod_Suc])));
 qed "fib_Cassini";