src/HOL/Fact.thy
changeset 32558 e6e1fc2e73cb
parent 32047 c141f139ce26
child 33319 74f0dcc0b5fb
--- a/src/HOL/Fact.thy	Thu Sep 10 15:23:09 2009 +0200
+++ b/src/HOL/Fact.thy	Thu Sep 10 15:26:51 2009 +0200
@@ -8,7 +8,7 @@
 header{*Factorial Function*}
 
 theory Fact
-imports NatTransfer
+imports Nat_Transfer
 begin
 
 class fact =