change imports to move Fact.thy outside Plain
authorhuffman
Mon, 23 Feb 2009 07:58:13 -0800
changeset 30073 a4ad0c08b7d9
parent 30072 4eecd8b9b6cf
child 30074 38ce654e1b05
change imports to move Fact.thy outside Plain
src/HOL/Fact.thy
src/HOL/Plain.thy
--- 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"
--- a/src/HOL/Plain.thy	Mon Feb 23 07:19:53 2009 -0800
+++ b/src/HOL/Plain.thy	Mon Feb 23 07:58:13 2009 -0800
@@ -1,7 +1,7 @@
 header {* Plain HOL *}
 
 theory Plain
-imports Datatype FunDef Record Extraction Divides Fact
+imports Datatype FunDef Record Extraction Divides
 begin
 
 text {*