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