--- 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];
--- 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";
--- 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
--- 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);
--- 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";