--- a/src/HOL/Fact.thy Mon Feb 23 07:19:53 2009 -0800 +++ b/src/HOL/Fact.thy Mon Feb 23 07:58:13 2009 -0800 @@ -7,7 +7,7 @@ header{*Factorial Function*} theory Fact -imports Nat +imports Main begin consts fact :: "nat => nat"