src/HOL/Fact.thy
changeset 30073 a4ad0c08b7d9
parent 29693 708dcf7dec9f
child 30082 43c5b7bfc791
     1.1 --- a/src/HOL/Fact.thy	Mon Feb 23 07:19:53 2009 -0800
     1.2 +++ b/src/HOL/Fact.thy	Mon Feb 23 07:58:13 2009 -0800
     1.3 @@ -7,7 +7,7 @@
     1.4  header{*Factorial Function*}
     1.5  
     1.6  theory Fact
     1.7 -imports Nat
     1.8 +imports Main
     1.9  begin
    1.10  
    1.11  consts fact :: "nat => nat"