src/HOL/Power.ML
changeset 13451 467bccacc051
parent 12196 a3be6b3a9c0b
child 13601 fd3e3d6b37b2
--- a/src/HOL/Power.ML	Mon Aug 05 14:27:55 2002 +0200
+++ b/src/HOL/Power.ML	Mon Aug 05 14:28:31 2002 +0200
@@ -176,9 +176,9 @@
 (*This is the well-known version, but it's harder to use because of the
   need to reason about division.*)
 Goal "k <= n ==> (Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k";
-by (asm_simp_tac
-    (simpset_of NatDef.thy addsimps [Suc_times_binomial_eq, 
-				  div_mult_self_is_m]) 1);
+by (asm_simp_tac (simpset()
+  addsimps [Suc_times_binomial_eq, div_mult_self_is_m, zero_less_Suc]
+  delsimps [mult_Suc, mult_Suc_right]) 1);
 qed "binomial_Suc_Suc_eq_times";
 
 (*Another version, with -1 instead of Suc.*)