Plain, Main form meeting points in import hierarchy
authorhaftmann
Wed Jan 28 11:03:16 2009 +0100 (2009-01-28)
changeset 2965424e73987bfe2
parent 29653 ece6a0e9f8af
child 29655 ac31940cfb69
Plain, Main form meeting points in import hierarchy
src/HOL/ATP_Linkup.thy
src/HOL/Lubs.thy
src/HOL/Parity.thy
src/HOL/Polynomial.thy
src/HOL/Recdef.thy
src/HOL/Relation_Power.thy
     1.1 --- a/src/HOL/ATP_Linkup.thy	Wed Jan 28 11:02:12 2009 +0100
     1.2 +++ b/src/HOL/ATP_Linkup.thy	Wed Jan 28 11:03:16 2009 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  header {* The Isabelle-ATP Linkup *}
     1.5  
     1.6  theory ATP_Linkup
     1.7 -imports Divides Record Hilbert_Choice
     1.8 +imports Divides Record Hilbert_Choice Plain
     1.9  uses
    1.10    "Tools/polyhash.ML"
    1.11    "Tools/res_clause.ML"
     2.1 --- a/src/HOL/Lubs.thy	Wed Jan 28 11:02:12 2009 +0100
     2.2 +++ b/src/HOL/Lubs.thy	Wed Jan 28 11:03:16 2009 +0100
     2.3 @@ -1,5 +1,4 @@
     2.4  (*  Title       : Lubs.thy
     2.5 -    ID          : $Id$
     2.6      Author      : Jacques D. Fleuriot
     2.7      Copyright   : 1998  University of Cambridge
     2.8  *)
     2.9 @@ -7,7 +6,7 @@
    2.10  header{*Definitions of Upper Bounds and Least Upper Bounds*}
    2.11  
    2.12  theory Lubs
    2.13 -imports Plain
    2.14 +imports Plain Main
    2.15  begin
    2.16  
    2.17  text{*Thanks to suggestions by James Margetson*}
     3.1 --- a/src/HOL/Parity.thy	Wed Jan 28 11:02:12 2009 +0100
     3.2 +++ b/src/HOL/Parity.thy	Wed Jan 28 11:03:16 2009 +0100
     3.3 @@ -5,7 +5,7 @@
     3.4  header {* Even and Odd for int and nat *}
     3.5  
     3.6  theory Parity
     3.7 -imports Plain Presburger
     3.8 +imports Plain Presburger Main
     3.9  begin
    3.10  
    3.11  class even_odd = 
     4.1 --- a/src/HOL/Polynomial.thy	Wed Jan 28 11:02:12 2009 +0100
     4.2 +++ b/src/HOL/Polynomial.thy	Wed Jan 28 11:03:16 2009 +0100
     4.3 @@ -6,7 +6,7 @@
     4.4  header {* Univariate Polynomials *}
     4.5  
     4.6  theory Polynomial
     4.7 -imports Plain SetInterval
     4.8 +imports Plain SetInterval Main
     4.9  begin
    4.10  
    4.11  subsection {* Definition of type @{text poly} *}
     5.1 --- a/src/HOL/Recdef.thy	Wed Jan 28 11:02:12 2009 +0100
     5.2 +++ b/src/HOL/Recdef.thy	Wed Jan 28 11:03:16 2009 +0100
     5.3 @@ -1,12 +1,11 @@
     5.4  (*  Title:      HOL/Recdef.thy
     5.5 -    ID:         $Id$
     5.6      Author:     Konrad Slind and Markus Wenzel, TU Muenchen
     5.7  *)
     5.8  
     5.9  header {* TFL: recursive function definitions *}
    5.10  
    5.11  theory Recdef
    5.12 -imports FunDef
    5.13 +imports FunDef Plain
    5.14  uses
    5.15    ("Tools/TFL/casesplit.ML")
    5.16    ("Tools/TFL/utils.ML")
     6.1 --- a/src/HOL/Relation_Power.thy	Wed Jan 28 11:02:12 2009 +0100
     6.2 +++ b/src/HOL/Relation_Power.thy	Wed Jan 28 11:03:16 2009 +0100
     6.3 @@ -1,5 +1,4 @@
     6.4  (*  Title:      HOL/Relation_Power.thy
     6.5 -    ID:         $Id$
     6.6      Author:     Tobias Nipkow
     6.7      Copyright   1996  TU Muenchen
     6.8  *)
     6.9 @@ -7,7 +6,7 @@
    6.10  header{*Powers of Relations and Functions*}
    6.11  
    6.12  theory Relation_Power
    6.13 -imports Power Transitive_Closure
    6.14 +imports Power Transitive_Closure Plain
    6.15  begin
    6.16  
    6.17  instance