# HG changeset patch
# User berghofe
# Date 1028550511 -7200
# Node ID 467bccacc0510ea7dc17e32a32feb8ecc8baf802
# Parent  17fec4798b91af5bd38a381907c42f76e4a29575
Removed reference to simpset of NatDef.thy

diff -r 17fec4798b91 -r 467bccacc051 src/HOL/Power.ML
--- 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.*)