src/HOL/Divides.ML
changeset 5537 c2bd39a2c0ee
parent 5498 7b81cae2774f
child 5983 79e301a6a51b
--- 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";