absolute imports of HOL/*.thy theories
authorhaftmann
Mon Jul 07 08:47:17 2008 +0200 (2008-07-07)
changeset 27487c8a6ce181805
parent 27486 c61507a98bff
child 27488 9771f949bd84
absolute imports of HOL/*.thy theories
src/HOL/Library/AssocList.thy
src/HOL/Library/BigO.thy
src/HOL/Library/Binomial.thy
src/HOL/Library/Char_nat.thy
src/HOL/Library/Code_Char.thy
src/HOL/Library/Code_Index.thy
src/HOL/Library/Code_Integer.thy
src/HOL/Library/Code_Message.thy
src/HOL/Library/Coinductive_List.thy
src/HOL/Library/Commutative_Ring.thy
src/HOL/Library/Continuity.thy
src/HOL/Library/Countable.thy
src/HOL/Library/Dense_Linear_Order.thy
src/HOL/Library/Enum.thy
src/HOL/Library/Eval_Witness.thy
src/HOL/Library/Executable_Set.thy
src/HOL/Library/FuncSet.thy
src/HOL/Library/GCD.thy
src/HOL/Library/Heap.thy
src/HOL/Library/Infinite_Set.thy
src/HOL/Library/LaTeXsugar.thy
src/HOL/Library/ListVector.thy
src/HOL/Library/List_Prefix.thy
src/HOL/Library/List_lexord.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/NatPair.thy
src/HOL/Library/Nat_Infinity.thy
src/HOL/Library/Nested_Environment.thy
src/HOL/Library/Numeral_Type.thy
src/HOL/Library/Order_Relation.thy
src/HOL/Library/Parity.thy
src/HOL/Library/Pocklington.thy
src/HOL/Library/Primes.thy
src/HOL/Library/Quotient.thy
src/HOL/Library/RType.thy
src/HOL/Library/Ramsey.thy
src/HOL/Library/State_Monad.thy
src/HOL/Library/Sublist_Order.thy
src/HOL/Library/Univ_Poly.thy
src/HOL/Library/While_Combinator.thy
src/HOL/Library/Word.thy
     1.1 --- a/src/HOL/Library/AssocList.thy	Fri Jul 04 16:33:08 2008 +0200
     1.2 +++ b/src/HOL/Library/AssocList.thy	Mon Jul 07 08:47:17 2008 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* Map operations implemented on association lists*}
     1.5  
     1.6  theory AssocList 
     1.7 -imports Plain Map
     1.8 +imports Plain "~~/src/HOL/Map"
     1.9  begin
    1.10  
    1.11  text {*
     2.1 --- a/src/HOL/Library/BigO.thy	Fri Jul 04 16:33:08 2008 +0200
     2.2 +++ b/src/HOL/Library/BigO.thy	Mon Jul 07 08:47:17 2008 +0200
     2.3 @@ -6,7 +6,7 @@
     2.4  header {* Big O notation *}
     2.5  
     2.6  theory BigO
     2.7 -imports Plain Presburger SetsAndFunctions
     2.8 +imports Plain "~~/src/HOL/Presburger" SetsAndFunctions
     2.9  begin
    2.10  
    2.11  text {*
     3.1 --- a/src/HOL/Library/Binomial.thy	Fri Jul 04 16:33:08 2008 +0200
     3.2 +++ b/src/HOL/Library/Binomial.thy	Mon Jul 07 08:47:17 2008 +0200
     3.3 @@ -7,7 +7,7 @@
     3.4  header {* Binomial Coefficients *}
     3.5  
     3.6  theory Binomial
     3.7 -imports Plain SetInterval
     3.8 +imports Plain "~~/src/HOL/SetInterval"
     3.9  begin
    3.10  
    3.11  text {* This development is based on the work of Andy Gordon and
     4.1 --- a/src/HOL/Library/Char_nat.thy	Fri Jul 04 16:33:08 2008 +0200
     4.2 +++ b/src/HOL/Library/Char_nat.thy	Mon Jul 07 08:47:17 2008 +0200
     4.3 @@ -6,7 +6,7 @@
     4.4  header {* Mapping between characters and natural numbers *}
     4.5  
     4.6  theory Char_nat
     4.7 -imports Plain List
     4.8 +imports Plain "~~/src/HOL/List"
     4.9  begin
    4.10  
    4.11  text {* Conversions between nibbles and natural numbers in [0..15]. *}
     5.1 --- a/src/HOL/Library/Code_Char.thy	Fri Jul 04 16:33:08 2008 +0200
     5.2 +++ b/src/HOL/Library/Code_Char.thy	Mon Jul 07 08:47:17 2008 +0200
     5.3 @@ -6,7 +6,7 @@
     5.4  header {* Code generation of pretty characters (and strings) *}
     5.5  
     5.6  theory Code_Char
     5.7 -imports Plain List
     5.8 +imports Plain "~~/src/HOL/List"
     5.9  begin
    5.10  
    5.11  declare char.recs [code func del] char.cases [code func del]
     6.1 --- a/src/HOL/Library/Code_Index.thy	Fri Jul 04 16:33:08 2008 +0200
     6.2 +++ b/src/HOL/Library/Code_Index.thy	Mon Jul 07 08:47:17 2008 +0200
     6.3 @@ -5,7 +5,7 @@
     6.4  header {* Type of indices *}
     6.5  
     6.6  theory Code_Index
     6.7 -imports Plain Presburger
     6.8 +imports Plain "~~/src/HOL/Presburger"
     6.9  begin
    6.10  
    6.11  text {*
     7.1 --- a/src/HOL/Library/Code_Integer.thy	Fri Jul 04 16:33:08 2008 +0200
     7.2 +++ b/src/HOL/Library/Code_Integer.thy	Mon Jul 07 08:47:17 2008 +0200
     7.3 @@ -6,7 +6,7 @@
     7.4  header {* Pretty integer literals for code generation *}
     7.5  
     7.6  theory Code_Integer
     7.7 -imports Plain Presburger
     7.8 +imports Plain "~~/src/HOL/Presburger"
     7.9  begin
    7.10  
    7.11  text {*
     8.1 --- a/src/HOL/Library/Code_Message.thy	Fri Jul 04 16:33:08 2008 +0200
     8.2 +++ b/src/HOL/Library/Code_Message.thy	Mon Jul 07 08:47:17 2008 +0200
     8.3 @@ -5,7 +5,7 @@
     8.4  header {* Monolithic strings (message strings) for code generation *}
     8.5  
     8.6  theory Code_Message
     8.7 -imports Plain List
     8.8 +imports Plain "~~/src/HOL/List"
     8.9  begin
    8.10  
    8.11  subsection {* Datatype of messages *}
     9.1 --- a/src/HOL/Library/Coinductive_List.thy	Fri Jul 04 16:33:08 2008 +0200
     9.2 +++ b/src/HOL/Library/Coinductive_List.thy	Mon Jul 07 08:47:17 2008 +0200
     9.3 @@ -6,7 +6,7 @@
     9.4  header {* Potentially infinite lists as greatest fixed-point *}
     9.5  
     9.6  theory Coinductive_List
     9.7 -imports Plain List
     9.8 +imports Plain "~~/src/HOL/List"
     9.9  begin
    9.10  
    9.11  subsection {* List constructors over the datatype universe *}
    10.1 --- a/src/HOL/Library/Commutative_Ring.thy	Fri Jul 04 16:33:08 2008 +0200
    10.2 +++ b/src/HOL/Library/Commutative_Ring.thy	Mon Jul 07 08:47:17 2008 +0200
    10.3 @@ -7,7 +7,7 @@
    10.4  header {* Proving equalities in commutative rings *}
    10.5  
    10.6  theory Commutative_Ring
    10.7 -imports Plain List Parity
    10.8 +imports Plain "~~/src/HOL/List" Parity
    10.9  uses ("comm_ring.ML")
   10.10  begin
   10.11  
    11.1 --- a/src/HOL/Library/Continuity.thy	Fri Jul 04 16:33:08 2008 +0200
    11.2 +++ b/src/HOL/Library/Continuity.thy	Mon Jul 07 08:47:17 2008 +0200
    11.3 @@ -6,7 +6,7 @@
    11.4  header {* Continuity and iterations (of set transformers) *}
    11.5  
    11.6  theory Continuity
    11.7 -imports Plain Relation_Power
    11.8 +imports Plain "~~/src/HOL/Relation_Power"
    11.9  begin
   11.10  
   11.11  subsection {* Continuity for complete lattices *}
    12.1 --- a/src/HOL/Library/Countable.thy	Fri Jul 04 16:33:08 2008 +0200
    12.2 +++ b/src/HOL/Library/Countable.thy	Mon Jul 07 08:47:17 2008 +0200
    12.3 @@ -6,7 +6,7 @@
    12.4  header {* Encoding (almost) everything into natural numbers *}
    12.5  
    12.6  theory Countable
    12.7 -imports Plain List Hilbert_Choice
    12.8 +imports Plain "~~/src/HOL/List" "~~/src/HOL/Hilbert_Choice"
    12.9  begin
   12.10  
   12.11  subsection {* The class of countable types *}
    13.1 --- a/src/HOL/Library/Dense_Linear_Order.thy	Fri Jul 04 16:33:08 2008 +0200
    13.2 +++ b/src/HOL/Library/Dense_Linear_Order.thy	Mon Jul 07 08:47:17 2008 +0200
    13.3 @@ -7,7 +7,7 @@
    13.4    and a quantifier elimination procedure in Ferrante and Rackoff style *}
    13.5  
    13.6  theory Dense_Linear_Order
    13.7 -imports Plain Presburger
    13.8 +imports Plain "~~/src/HOL/Presburger"
    13.9  uses
   13.10    "~~/src/HOL/Tools/Qelim/qelim.ML"
   13.11    "~~/src/HOL/Tools/Qelim/langford_data.ML"
    14.1 --- a/src/HOL/Library/Enum.thy	Fri Jul 04 16:33:08 2008 +0200
    14.2 +++ b/src/HOL/Library/Enum.thy	Mon Jul 07 08:47:17 2008 +0200
    14.3 @@ -6,7 +6,7 @@
    14.4  header {* Finite types as explicit enumerations *}
    14.5  
    14.6  theory Enum
    14.7 -imports Plain Map
    14.8 +imports Plain "~~/src/HOL/Map"
    14.9  begin
   14.10  
   14.11  subsection {* Class @{text enum} *}
    15.1 --- a/src/HOL/Library/Eval_Witness.thy	Fri Jul 04 16:33:08 2008 +0200
    15.2 +++ b/src/HOL/Library/Eval_Witness.thy	Mon Jul 07 08:47:17 2008 +0200
    15.3 @@ -7,7 +7,7 @@
    15.4  header {* Evaluation Oracle with ML witnesses *}
    15.5  
    15.6  theory Eval_Witness
    15.7 -imports Plain List
    15.8 +imports Plain "~~/src/HOL/List"
    15.9  begin
   15.10  
   15.11  text {* 
    16.1 --- a/src/HOL/Library/Executable_Set.thy	Fri Jul 04 16:33:08 2008 +0200
    16.2 +++ b/src/HOL/Library/Executable_Set.thy	Mon Jul 07 08:47:17 2008 +0200
    16.3 @@ -6,7 +6,7 @@
    16.4  header {* Implementation of finite sets by lists *}
    16.5  
    16.6  theory Executable_Set
    16.7 -imports Plain List
    16.8 +imports Plain "~~/src/HOL/List"
    16.9  begin
   16.10  
   16.11  subsection {* Definitional rewrites *}
    17.1 --- a/src/HOL/Library/FuncSet.thy	Fri Jul 04 16:33:08 2008 +0200
    17.2 +++ b/src/HOL/Library/FuncSet.thy	Mon Jul 07 08:47:17 2008 +0200
    17.3 @@ -6,7 +6,7 @@
    17.4  header {* Pi and Function Sets *}
    17.5  
    17.6  theory FuncSet
    17.7 -imports Plain Hilbert_Choice
    17.8 +imports Plain "~~/src/HOL/Hilbert_Choice"
    17.9  begin
   17.10  
   17.11  definition
    18.1 --- a/src/HOL/Library/GCD.thy	Fri Jul 04 16:33:08 2008 +0200
    18.2 +++ b/src/HOL/Library/GCD.thy	Mon Jul 07 08:47:17 2008 +0200
    18.3 @@ -7,7 +7,7 @@
    18.4  header {* The Greatest Common Divisor *}
    18.5  
    18.6  theory GCD
    18.7 -imports Plain Presburger
    18.8 +imports Plain "~~/src/HOL/Presburger"
    18.9  begin
   18.10  
   18.11  text {*
    19.1 --- a/src/HOL/Library/Heap.thy	Fri Jul 04 16:33:08 2008 +0200
    19.2 +++ b/src/HOL/Library/Heap.thy	Mon Jul 07 08:47:17 2008 +0200
    19.3 @@ -6,7 +6,7 @@
    19.4  header {* A polymorphic heap based on cantor encodings *}
    19.5  
    19.6  theory Heap
    19.7 -imports Plain List Countable RType
    19.8 +imports Plain "~~/src/HOL/List" Countable RType
    19.9  begin
   19.10  
   19.11  subsection {* Representable types *}
    20.1 --- a/src/HOL/Library/Infinite_Set.thy	Fri Jul 04 16:33:08 2008 +0200
    20.2 +++ b/src/HOL/Library/Infinite_Set.thy	Mon Jul 07 08:47:17 2008 +0200
    20.3 @@ -6,7 +6,7 @@
    20.4  header {* Infinite Sets and Related Concepts *}
    20.5  
    20.6  theory Infinite_Set
    20.7 -imports Plain SetInterval Hilbert_Choice
    20.8 +imports Plain "~~/src/HOL/SetInterval" "~~/src/HOL/Hilbert_Choice"
    20.9  begin
   20.10  
   20.11  
    21.1 --- a/src/HOL/Library/LaTeXsugar.thy	Fri Jul 04 16:33:08 2008 +0200
    21.2 +++ b/src/HOL/Library/LaTeXsugar.thy	Mon Jul 07 08:47:17 2008 +0200
    21.3 @@ -6,7 +6,7 @@
    21.4  
    21.5  (*<*)
    21.6  theory LaTeXsugar
    21.7 -imports Plain List
    21.8 +imports Plain "~~/src/HOL/List"
    21.9  begin
   21.10  
   21.11  (* LOGIC *)
    22.1 --- a/src/HOL/Library/ListVector.thy	Fri Jul 04 16:33:08 2008 +0200
    22.2 +++ b/src/HOL/Library/ListVector.thy	Mon Jul 07 08:47:17 2008 +0200
    22.3 @@ -5,7 +5,7 @@
    22.4  header "Lists as vectors"
    22.5  
    22.6  theory ListVector
    22.7 -imports Plain List
    22.8 +imports Plain "~~/src/HOL/List"
    22.9  begin
   22.10  
   22.11  text{* \noindent
    23.1 --- a/src/HOL/Library/List_Prefix.thy	Fri Jul 04 16:33:08 2008 +0200
    23.2 +++ b/src/HOL/Library/List_Prefix.thy	Mon Jul 07 08:47:17 2008 +0200
    23.3 @@ -6,7 +6,7 @@
    23.4  header {* List prefixes and postfixes *}
    23.5  
    23.6  theory List_Prefix
    23.7 -imports Plain List
    23.8 +imports Plain "~~/src/HOL/List"
    23.9  begin
   23.10  
   23.11  subsection {* Prefix order on lists *}
    24.1 --- a/src/HOL/Library/List_lexord.thy	Fri Jul 04 16:33:08 2008 +0200
    24.2 +++ b/src/HOL/Library/List_lexord.thy	Mon Jul 07 08:47:17 2008 +0200
    24.3 @@ -6,7 +6,7 @@
    24.4  header {* Lexicographic order on lists *}
    24.5  
    24.6  theory List_lexord
    24.7 -imports Plain List
    24.8 +imports Plain "~~/src/HOL/List"
    24.9  begin
   24.10  
   24.11  instantiation list :: (ord) ord
    25.1 --- a/src/HOL/Library/Multiset.thy	Fri Jul 04 16:33:08 2008 +0200
    25.2 +++ b/src/HOL/Library/Multiset.thy	Mon Jul 07 08:47:17 2008 +0200
    25.3 @@ -6,7 +6,7 @@
    25.4  header {* Multisets *}
    25.5  
    25.6  theory Multiset
    25.7 -imports Plain List
    25.8 +imports Plain "~~/src/HOL/List"
    25.9  begin
   25.10  
   25.11  subsection {* The type of multisets *}
    26.1 --- a/src/HOL/Library/NatPair.thy	Fri Jul 04 16:33:08 2008 +0200
    26.2 +++ b/src/HOL/Library/NatPair.thy	Mon Jul 07 08:47:17 2008 +0200
    26.3 @@ -7,7 +7,7 @@
    26.4  header {* Pairs of Natural Numbers *}
    26.5  
    26.6  theory NatPair
    26.7 -imports Plain Presburger
    26.8 +imports Plain "~~/src/HOL/Presburger"
    26.9  begin
   26.10  
   26.11  text{*
    27.1 --- a/src/HOL/Library/Nat_Infinity.thy	Fri Jul 04 16:33:08 2008 +0200
    27.2 +++ b/src/HOL/Library/Nat_Infinity.thy	Mon Jul 07 08:47:17 2008 +0200
    27.3 @@ -6,7 +6,7 @@
    27.4  header {* Natural numbers with infinity *}
    27.5  
    27.6  theory Nat_Infinity
    27.7 -imports Plain Presburger
    27.8 +imports Plain "~~/src/HOL/Presburger"
    27.9  begin
   27.10  
   27.11  subsection {* Type definition *}
    28.1 --- a/src/HOL/Library/Nested_Environment.thy	Fri Jul 04 16:33:08 2008 +0200
    28.2 +++ b/src/HOL/Library/Nested_Environment.thy	Mon Jul 07 08:47:17 2008 +0200
    28.3 @@ -6,7 +6,7 @@
    28.4  header {* Nested environments *}
    28.5  
    28.6  theory Nested_Environment
    28.7 -imports Plain List
    28.8 +imports Plain "~~/src/HOL/List"
    28.9  begin
   28.10  
   28.11  text {*
    29.1 --- a/src/HOL/Library/Numeral_Type.thy	Fri Jul 04 16:33:08 2008 +0200
    29.2 +++ b/src/HOL/Library/Numeral_Type.thy	Mon Jul 07 08:47:17 2008 +0200
    29.3 @@ -8,7 +8,7 @@
    29.4  header "Numeral Syntax for Types"
    29.5  
    29.6  theory Numeral_Type
    29.7 -imports Plain Presburger
    29.8 +imports Plain "~~/src/HOL/Presburger"
    29.9  begin
   29.10  
   29.11  subsection {* Preliminary lemmas *}
    30.1 --- a/src/HOL/Library/Order_Relation.thy	Fri Jul 04 16:33:08 2008 +0200
    30.2 +++ b/src/HOL/Library/Order_Relation.thy	Mon Jul 07 08:47:17 2008 +0200
    30.3 @@ -5,7 +5,7 @@
    30.4  header {* Orders as Relations *}
    30.5  
    30.6  theory Order_Relation
    30.7 -imports Plain Hilbert_Choice ATP_Linkup
    30.8 +imports Plain "~~/src/HOL/Hilbert_Choice" "~~/src/HOL/ATP_Linkup"
    30.9  begin
   30.10  
   30.11  text{* This prelude could be moved to theory Relation: *}
    31.1 --- a/src/HOL/Library/Parity.thy	Fri Jul 04 16:33:08 2008 +0200
    31.2 +++ b/src/HOL/Library/Parity.thy	Mon Jul 07 08:47:17 2008 +0200
    31.3 @@ -6,7 +6,7 @@
    31.4  header {* Even and Odd for int and nat *}
    31.5  
    31.6  theory Parity
    31.7 -imports Plain Presburger
    31.8 +imports Plain "~~/src/HOL/Presburger"
    31.9  begin
   31.10  
   31.11  class even_odd = type + 
    32.1 --- a/src/HOL/Library/Pocklington.thy	Fri Jul 04 16:33:08 2008 +0200
    32.2 +++ b/src/HOL/Library/Pocklington.thy	Mon Jul 07 08:47:17 2008 +0200
    32.3 @@ -7,7 +7,7 @@
    32.4  
    32.5  
    32.6  theory Pocklington
    32.7 -imports Plain List Primes
    32.8 +imports Plain "~~/src/HOL/List" "~~/src/HOL/Primes"
    32.9  begin
   32.10  
   32.11  definition modeq:: "nat => nat => nat => bool"    ("(1[_ = _] '(mod _'))")
    33.1 --- a/src/HOL/Library/Primes.thy	Fri Jul 04 16:33:08 2008 +0200
    33.2 +++ b/src/HOL/Library/Primes.thy	Mon Jul 07 08:47:17 2008 +0200
    33.3 @@ -7,7 +7,7 @@
    33.4  header {* Primality on nat *}
    33.5  
    33.6  theory Primes
    33.7 -imports Plain ATP_Linkup GCD Parity
    33.8 +imports Plain "~~/src/HOL/ATP_Linkup" GCD Parity
    33.9  begin
   33.10  
   33.11  definition
    34.1 --- a/src/HOL/Library/Quotient.thy	Fri Jul 04 16:33:08 2008 +0200
    34.2 +++ b/src/HOL/Library/Quotient.thy	Mon Jul 07 08:47:17 2008 +0200
    34.3 @@ -6,7 +6,7 @@
    34.4  header {* Quotient types *}
    34.5  
    34.6  theory Quotient
    34.7 -imports Plain Hilbert_Choice
    34.8 +imports Plain "~~/src/HOL/Hilbert_Choice"
    34.9  begin
   34.10  
   34.11  text {*
    35.1 --- a/src/HOL/Library/RType.thy	Fri Jul 04 16:33:08 2008 +0200
    35.2 +++ b/src/HOL/Library/RType.thy	Mon Jul 07 08:47:17 2008 +0200
    35.3 @@ -6,7 +6,7 @@
    35.4  header {* Reflecting Pure types into HOL *}
    35.5  
    35.6  theory RType
    35.7 -imports Plain List Code_Message Code_Index (* import all 'special code' types *)
    35.8 +imports Plain "~~/src/HOL/List" "~~/src/HOL/Code_Message" "~~/src/HOL/Code_Index" (* import all 'special code' types *)
    35.9  begin
   35.10  
   35.11  datatype "rtype" = RType message_string "rtype list"
    36.1 --- a/src/HOL/Library/Ramsey.thy	Fri Jul 04 16:33:08 2008 +0200
    36.2 +++ b/src/HOL/Library/Ramsey.thy	Mon Jul 07 08:47:17 2008 +0200
    36.3 @@ -6,7 +6,7 @@
    36.4  header "Ramsey's Theorem"
    36.5  
    36.6  theory Ramsey
    36.7 -imports Plain Presburger Infinite_Set
    36.8 +imports Plain "~~/src/HOL/Presburger" Infinite_Set
    36.9  begin
   36.10  
   36.11  subsection {* Preliminaries *}
    37.1 --- a/src/HOL/Library/State_Monad.thy	Fri Jul 04 16:33:08 2008 +0200
    37.2 +++ b/src/HOL/Library/State_Monad.thy	Mon Jul 07 08:47:17 2008 +0200
    37.3 @@ -3,10 +3,10 @@
    37.4      Author:     Florian Haftmann, TU Muenchen
    37.5  *)
    37.6  
    37.7 -header {* Combinators syntax for generic, open state monads (single threaded monads) *}
    37.8 +header {* Combinator syntax for generic, open state monads (single threaded monads) *}
    37.9  
   37.10  theory State_Monad
   37.11 -imports Plain List
   37.12 +imports Plain "~~/src/HOL/List"
   37.13  begin
   37.14  
   37.15  subsection {* Motivation *}
    38.1 --- a/src/HOL/Library/Sublist_Order.thy	Fri Jul 04 16:33:08 2008 +0200
    38.2 +++ b/src/HOL/Library/Sublist_Order.thy	Mon Jul 07 08:47:17 2008 +0200
    38.3 @@ -7,7 +7,7 @@
    38.4  header {* Sublist Ordering *}
    38.5  
    38.6  theory Sublist_Order
    38.7 -imports Plain List
    38.8 +imports Plain "~~/src/HOL/List"
    38.9  begin
   38.10  
   38.11  text {*
    39.1 --- a/src/HOL/Library/Univ_Poly.thy	Fri Jul 04 16:33:08 2008 +0200
    39.2 +++ b/src/HOL/Library/Univ_Poly.thy	Mon Jul 07 08:47:17 2008 +0200
    39.3 @@ -6,7 +6,7 @@
    39.4  header{*Univariate Polynomials*}
    39.5  
    39.6  theory Univ_Poly
    39.7 -imports Plain "../List"
    39.8 +imports Plain "~~/src/HOL/List"
    39.9  begin
   39.10  
   39.11  text{* Application of polynomial as a function. *}
    40.1 --- a/src/HOL/Library/While_Combinator.thy	Fri Jul 04 16:33:08 2008 +0200
    40.2 +++ b/src/HOL/Library/While_Combinator.thy	Mon Jul 07 08:47:17 2008 +0200
    40.3 @@ -7,7 +7,7 @@
    40.4  header {* A general ``while'' combinator *}
    40.5  
    40.6  theory While_Combinator
    40.7 -imports Plain Presburger
    40.8 +imports Plain "~~/src/HOL/Presburger"
    40.9  begin
   40.10  
   40.11  text {* 
    41.1 --- a/src/HOL/Library/Word.thy	Fri Jul 04 16:33:08 2008 +0200
    41.2 +++ b/src/HOL/Library/Word.thy	Mon Jul 07 08:47:17 2008 +0200
    41.3 @@ -6,7 +6,7 @@
    41.4  header {* Binary Words *}
    41.5  
    41.6  theory Word
    41.7 -imports Main
    41.8 +imports "~~/src/HOL/Main"
    41.9  begin
   41.10  
   41.11  subsection {* Auxilary Lemmas *}