# HG changeset patch
# User wenzelm
# Date 964475631 -7200
# Node ID 234ef8652caed1e10d37969c20a9ab564a1e2b49
# Parent  7aa79267fa82bb74567fc12e01f4ca65ef4286e0
simpset_of NatDef.thy (why anyway?);

diff -r 7aa79267fa82 -r 234ef8652cae src/HOL/Power.ML
--- a/src/HOL/Power.ML	Mon Jul 24 23:52:55 2000 +0200
+++ b/src/HOL/Power.ML	Mon Jul 24 23:53:51 2000 +0200
@@ -114,7 +114,7 @@
 
 Goal "k <= n ==> (Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k";
 by (asm_simp_tac
-    (simpset_of Nat.thy addsimps [Suc_times_binomial_eq, 
+    (simpset_of NatDef.thy addsimps [Suc_times_binomial_eq, 
 				  div_mult_self_is_m]) 1);
 qed "binomial_Suc_Suc_eq_times";