--- 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.*)