Plain, Main form meeting points in import hierarchy
authorhaftmann
Wed Jan 28 11:03:42 2009 +0100 (2009-01-28)
changeset 29655ac31940cfb69
parent 29654 24e73987bfe2
child 29656 bd6fb191c00e
Plain, Main form meeting points in import hierarchy
src/HOL/Dense_Linear_Order.thy
src/HOL/Equiv_Relations.thy
src/HOL/GCD.thy
src/HOL/Hilbert_Choice.thy
     1.1 --- a/src/HOL/Dense_Linear_Order.thy	Wed Jan 28 11:03:16 2009 +0100
     1.2 +++ b/src/HOL/Dense_Linear_Order.thy	Wed Jan 28 11:03:42 2009 +0100
     1.3 @@ -1,10 +1,12 @@
     1.4 -(* Author: Amine Chaieb, TU Muenchen *)
     1.5 +(*  Title       : HOL/Dense_Linear_Order.thy
     1.6 +    Author      : Amine Chaieb, TU Muenchen
     1.7 +*)
     1.8  
     1.9  header {* Dense linear order without endpoints
    1.10    and a quantifier elimination procedure in Ferrante and Rackoff style *}
    1.11  
    1.12  theory Dense_Linear_Order
    1.13 -imports Plain Groebner_Basis
    1.14 +imports Plain Groebner_Basis Main
    1.15  uses
    1.16    "~~/src/HOL/Tools/Qelim/langford_data.ML"
    1.17    "~~/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML"
     2.1 --- a/src/HOL/Equiv_Relations.thy	Wed Jan 28 11:03:16 2009 +0100
     2.2 +++ b/src/HOL/Equiv_Relations.thy	Wed Jan 28 11:03:42 2009 +0100
     2.3 @@ -1,12 +1,11 @@
     2.4 -(*  ID:         $Id$
     2.5 -    Authors:    Lawrence C Paulson, Cambridge University Computer Laboratory
     2.6 +(*  Authors:    Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7      Copyright   1996  University of Cambridge
     2.8  *)
     2.9  
    2.10  header {* Equivalence Relations in Higher-Order Set Theory *}
    2.11  
    2.12  theory Equiv_Relations
    2.13 -imports Finite_Set Relation
    2.14 +imports Finite_Set Relation Plain
    2.15  begin
    2.16  
    2.17  subsection {* Equivalence relations *}
     3.1 --- a/src/HOL/GCD.thy	Wed Jan 28 11:03:16 2009 +0100
     3.2 +++ b/src/HOL/GCD.thy	Wed Jan 28 11:03:42 2009 +0100
     3.3 @@ -1,5 +1,4 @@
     3.4  (*  Title:      HOL/GCD.thy
     3.5 -    ID:         $Id$
     3.6      Author:     Christophe Tabacznyj and Lawrence C Paulson
     3.7      Copyright   1996  University of Cambridge
     3.8  *)
     3.9 @@ -7,7 +6,7 @@
    3.10  header {* The Greatest Common Divisor *}
    3.11  
    3.12  theory GCD
    3.13 -imports Plain Presburger
    3.14 +imports Plain Presburger Main
    3.15  begin
    3.16  
    3.17  text {*
     4.1 --- a/src/HOL/Hilbert_Choice.thy	Wed Jan 28 11:03:16 2009 +0100
     4.2 +++ b/src/HOL/Hilbert_Choice.thy	Wed Jan 28 11:03:42 2009 +0100
     4.3 @@ -1,5 +1,4 @@
     4.4  (*  Title:      HOL/Hilbert_Choice.thy
     4.5 -    ID:         $Id$
     4.6      Author:     Lawrence C Paulson
     4.7      Copyright   2001  University of Cambridge
     4.8  *)
     4.9 @@ -7,7 +6,7 @@
    4.10  header {* Hilbert's Epsilon-Operator and the Axiom of Choice *}
    4.11  
    4.12  theory Hilbert_Choice
    4.13 -imports Nat Wellfounded
    4.14 +imports Nat Wellfounded Plain
    4.15  uses ("Tools/meson.ML") ("Tools/specification_package.ML")
    4.16  begin
    4.17