src/HOL/Hyperreal/Fact.thy

--- a/src/HOL/Hyperreal/Fact.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Hyperreal/Fact.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -6,7 +6,9 @@
 
 header{*Factorial Function*}
 
-theory Fact = Real:
+theory Fact
+import Real
+begin
 
 consts fact :: "nat => nat"
 primrec
@@ -71,4 +73,4 @@
 by (case_tac "m", auto)
 
 
-end
\ No newline at end of file
+end