--- a/src/HOL/Library/AssocList.thy Fri Jul 04 16:33:08 2008 +0200
+++ b/src/HOL/Library/AssocList.thy Mon Jul 07 08:47:17 2008 +0200
@@ -6,7 +6,7 @@
header {* Map operations implemented on association lists*}
theory AssocList
-imports Plain Map
+imports Plain "~~/src/HOL/Map"
begin
text {*
--- a/src/HOL/Library/BigO.thy Fri Jul 04 16:33:08 2008 +0200
+++ b/src/HOL/Library/BigO.thy Mon Jul 07 08:47:17 2008 +0200
@@ -6,7 +6,7 @@
header {* Big O notation *}
theory BigO
-imports Plain Presburger SetsAndFunctions
+imports Plain "~~/src/HOL/Presburger" SetsAndFunctions
begin
text {*
--- a/src/HOL/Library/Binomial.thy Fri Jul 04 16:33:08 2008 +0200
+++ b/src/HOL/Library/Binomial.thy Mon Jul 07 08:47:17 2008 +0200
@@ -7,7 +7,7 @@
header {* Binomial Coefficients *}
theory Binomial
-imports Plain SetInterval
+imports Plain "~~/src/HOL/SetInterval"
begin
text {* This development is based on the work of Andy Gordon and
--- a/src/HOL/Library/Char_nat.thy Fri Jul 04 16:33:08 2008 +0200
+++ b/src/HOL/Library/Char_nat.thy Mon Jul 07 08:47:17 2008 +0200
@@ -6,7 +6,7 @@
header {* Mapping between characters and natural numbers *}
theory Char_nat
-imports Plain List
+imports Plain "~~/src/HOL/List"
begin
text {* Conversions between nibbles and natural numbers in [0..15]. *}
--- a/src/HOL/Library/Code_Char.thy Fri Jul 04 16:33:08 2008 +0200
+++ b/src/HOL/Library/Code_Char.thy Mon Jul 07 08:47:17 2008 +0200
@@ -6,7 +6,7 @@
header {* Code generation of pretty characters (and strings) *}
theory Code_Char
-imports Plain List
+imports Plain "~~/src/HOL/List"
begin
declare char.recs [code func del] char.cases [code func del]
--- a/src/HOL/Library/Code_Index.thy Fri Jul 04 16:33:08 2008 +0200
+++ b/src/HOL/Library/Code_Index.thy Mon Jul 07 08:47:17 2008 +0200
@@ -5,7 +5,7 @@
header {* Type of indices *}
theory Code_Index
-imports Plain Presburger
+imports Plain "~~/src/HOL/Presburger"
begin
text {*
--- a/src/HOL/Library/Code_Integer.thy Fri Jul 04 16:33:08 2008 +0200
+++ b/src/HOL/Library/Code_Integer.thy Mon Jul 07 08:47:17 2008 +0200
@@ -6,7 +6,7 @@
header {* Pretty integer literals for code generation *}
theory Code_Integer
-imports Plain Presburger
+imports Plain "~~/src/HOL/Presburger"
begin
text {*
--- a/src/HOL/Library/Code_Message.thy Fri Jul 04 16:33:08 2008 +0200
+++ b/src/HOL/Library/Code_Message.thy Mon Jul 07 08:47:17 2008 +0200
@@ -5,7 +5,7 @@
header {* Monolithic strings (message strings) for code generation *}
theory Code_Message
-imports Plain List
+imports Plain "~~/src/HOL/List"
begin
subsection {* Datatype of messages *}
--- a/src/HOL/Library/Coinductive_List.thy Fri Jul 04 16:33:08 2008 +0200
+++ b/src/HOL/Library/Coinductive_List.thy Mon Jul 07 08:47:17 2008 +0200
@@ -6,7 +6,7 @@
header {* Potentially infinite lists as greatest fixed-point *}
theory Coinductive_List
-imports Plain List
+imports Plain "~~/src/HOL/List"
begin
subsection {* List constructors over the datatype universe *}
--- a/src/HOL/Library/Commutative_Ring.thy Fri Jul 04 16:33:08 2008 +0200
+++ b/src/HOL/Library/Commutative_Ring.thy Mon Jul 07 08:47:17 2008 +0200
@@ -7,7 +7,7 @@
header {* Proving equalities in commutative rings *}
theory Commutative_Ring
-imports Plain List Parity
+imports Plain "~~/src/HOL/List" Parity
uses ("comm_ring.ML")
begin
--- a/src/HOL/Library/Continuity.thy Fri Jul 04 16:33:08 2008 +0200
+++ b/src/HOL/Library/Continuity.thy Mon Jul 07 08:47:17 2008 +0200
@@ -6,7 +6,7 @@
header {* Continuity and iterations (of set transformers) *}
theory Continuity
-imports Plain Relation_Power
+imports Plain "~~/src/HOL/Relation_Power"
begin
subsection {* Continuity for complete lattices *}
--- a/src/HOL/Library/Countable.thy Fri Jul 04 16:33:08 2008 +0200
+++ b/src/HOL/Library/Countable.thy Mon Jul 07 08:47:17 2008 +0200
@@ -6,7 +6,7 @@
header {* Encoding (almost) everything into natural numbers *}
theory Countable
-imports Plain List Hilbert_Choice
+imports Plain "~~/src/HOL/List" "~~/src/HOL/Hilbert_Choice"
begin
subsection {* The class of countable types *}
--- a/src/HOL/Library/Dense_Linear_Order.thy Fri Jul 04 16:33:08 2008 +0200
+++ b/src/HOL/Library/Dense_Linear_Order.thy Mon Jul 07 08:47:17 2008 +0200
@@ -7,7 +7,7 @@
and a quantifier elimination procedure in Ferrante and Rackoff style *}
theory Dense_Linear_Order
-imports Plain Presburger
+imports Plain "~~/src/HOL/Presburger"
uses
"~~/src/HOL/Tools/Qelim/qelim.ML"
"~~/src/HOL/Tools/Qelim/langford_data.ML"
--- a/src/HOL/Library/Enum.thy Fri Jul 04 16:33:08 2008 +0200
+++ b/src/HOL/Library/Enum.thy Mon Jul 07 08:47:17 2008 +0200
@@ -6,7 +6,7 @@
header {* Finite types as explicit enumerations *}
theory Enum
-imports Plain Map
+imports Plain "~~/src/HOL/Map"
begin
subsection {* Class @{text enum} *}
--- a/src/HOL/Library/Eval_Witness.thy Fri Jul 04 16:33:08 2008 +0200
+++ b/src/HOL/Library/Eval_Witness.thy Mon Jul 07 08:47:17 2008 +0200
@@ -7,7 +7,7 @@
header {* Evaluation Oracle with ML witnesses *}
theory Eval_Witness
-imports Plain List
+imports Plain "~~/src/HOL/List"
begin
text {*
--- a/src/HOL/Library/Executable_Set.thy Fri Jul 04 16:33:08 2008 +0200
+++ b/src/HOL/Library/Executable_Set.thy Mon Jul 07 08:47:17 2008 +0200
@@ -6,7 +6,7 @@
header {* Implementation of finite sets by lists *}
theory Executable_Set
-imports Plain List
+imports Plain "~~/src/HOL/List"
begin
subsection {* Definitional rewrites *}
--- a/src/HOL/Library/FuncSet.thy Fri Jul 04 16:33:08 2008 +0200
+++ b/src/HOL/Library/FuncSet.thy Mon Jul 07 08:47:17 2008 +0200
@@ -6,7 +6,7 @@
header {* Pi and Function Sets *}
theory FuncSet
-imports Plain Hilbert_Choice
+imports Plain "~~/src/HOL/Hilbert_Choice"
begin
definition
--- a/src/HOL/Library/GCD.thy Fri Jul 04 16:33:08 2008 +0200
+++ b/src/HOL/Library/GCD.thy Mon Jul 07 08:47:17 2008 +0200
@@ -7,7 +7,7 @@
header {* The Greatest Common Divisor *}
theory GCD
-imports Plain Presburger
+imports Plain "~~/src/HOL/Presburger"
begin
text {*
--- a/src/HOL/Library/Heap.thy Fri Jul 04 16:33:08 2008 +0200
+++ b/src/HOL/Library/Heap.thy Mon Jul 07 08:47:17 2008 +0200
@@ -6,7 +6,7 @@
header {* A polymorphic heap based on cantor encodings *}
theory Heap
-imports Plain List Countable RType
+imports Plain "~~/src/HOL/List" Countable RType
begin
subsection {* Representable types *}
--- a/src/HOL/Library/Infinite_Set.thy Fri Jul 04 16:33:08 2008 +0200
+++ b/src/HOL/Library/Infinite_Set.thy Mon Jul 07 08:47:17 2008 +0200
@@ -6,7 +6,7 @@
header {* Infinite Sets and Related Concepts *}
theory Infinite_Set
-imports Plain SetInterval Hilbert_Choice
+imports Plain "~~/src/HOL/SetInterval" "~~/src/HOL/Hilbert_Choice"
begin
--- a/src/HOL/Library/LaTeXsugar.thy Fri Jul 04 16:33:08 2008 +0200
+++ b/src/HOL/Library/LaTeXsugar.thy Mon Jul 07 08:47:17 2008 +0200
@@ -6,7 +6,7 @@
(*<*)
theory LaTeXsugar
-imports Plain List
+imports Plain "~~/src/HOL/List"
begin
(* LOGIC *)
--- a/src/HOL/Library/ListVector.thy Fri Jul 04 16:33:08 2008 +0200
+++ b/src/HOL/Library/ListVector.thy Mon Jul 07 08:47:17 2008 +0200
@@ -5,7 +5,7 @@
header "Lists as vectors"
theory ListVector
-imports Plain List
+imports Plain "~~/src/HOL/List"
begin
text{* \noindent
--- a/src/HOL/Library/List_Prefix.thy Fri Jul 04 16:33:08 2008 +0200
+++ b/src/HOL/Library/List_Prefix.thy Mon Jul 07 08:47:17 2008 +0200
@@ -6,7 +6,7 @@
header {* List prefixes and postfixes *}
theory List_Prefix
-imports Plain List
+imports Plain "~~/src/HOL/List"
begin
subsection {* Prefix order on lists *}
--- a/src/HOL/Library/List_lexord.thy Fri Jul 04 16:33:08 2008 +0200
+++ b/src/HOL/Library/List_lexord.thy Mon Jul 07 08:47:17 2008 +0200
@@ -6,7 +6,7 @@
header {* Lexicographic order on lists *}
theory List_lexord
-imports Plain List
+imports Plain "~~/src/HOL/List"
begin
instantiation list :: (ord) ord
--- a/src/HOL/Library/Multiset.thy Fri Jul 04 16:33:08 2008 +0200
+++ b/src/HOL/Library/Multiset.thy Mon Jul 07 08:47:17 2008 +0200
@@ -6,7 +6,7 @@
header {* Multisets *}
theory Multiset
-imports Plain List
+imports Plain "~~/src/HOL/List"
begin
subsection {* The type of multisets *}
--- a/src/HOL/Library/NatPair.thy Fri Jul 04 16:33:08 2008 +0200
+++ b/src/HOL/Library/NatPair.thy Mon Jul 07 08:47:17 2008 +0200
@@ -7,7 +7,7 @@
header {* Pairs of Natural Numbers *}
theory NatPair
-imports Plain Presburger
+imports Plain "~~/src/HOL/Presburger"
begin
text{*
--- a/src/HOL/Library/Nat_Infinity.thy Fri Jul 04 16:33:08 2008 +0200
+++ b/src/HOL/Library/Nat_Infinity.thy Mon Jul 07 08:47:17 2008 +0200
@@ -6,7 +6,7 @@
header {* Natural numbers with infinity *}
theory Nat_Infinity
-imports Plain Presburger
+imports Plain "~~/src/HOL/Presburger"
begin
subsection {* Type definition *}
--- a/src/HOL/Library/Nested_Environment.thy Fri Jul 04 16:33:08 2008 +0200
+++ b/src/HOL/Library/Nested_Environment.thy Mon Jul 07 08:47:17 2008 +0200
@@ -6,7 +6,7 @@
header {* Nested environments *}
theory Nested_Environment
-imports Plain List
+imports Plain "~~/src/HOL/List"
begin
text {*
--- a/src/HOL/Library/Numeral_Type.thy Fri Jul 04 16:33:08 2008 +0200
+++ b/src/HOL/Library/Numeral_Type.thy Mon Jul 07 08:47:17 2008 +0200
@@ -8,7 +8,7 @@
header "Numeral Syntax for Types"
theory Numeral_Type
-imports Plain Presburger
+imports Plain "~~/src/HOL/Presburger"
begin
subsection {* Preliminary lemmas *}
--- a/src/HOL/Library/Order_Relation.thy Fri Jul 04 16:33:08 2008 +0200
+++ b/src/HOL/Library/Order_Relation.thy Mon Jul 07 08:47:17 2008 +0200
@@ -5,7 +5,7 @@
header {* Orders as Relations *}
theory Order_Relation
-imports Plain Hilbert_Choice ATP_Linkup
+imports Plain "~~/src/HOL/Hilbert_Choice" "~~/src/HOL/ATP_Linkup"
begin
text{* This prelude could be moved to theory Relation: *}
--- a/src/HOL/Library/Parity.thy Fri Jul 04 16:33:08 2008 +0200
+++ b/src/HOL/Library/Parity.thy Mon Jul 07 08:47:17 2008 +0200
@@ -6,7 +6,7 @@
header {* Even and Odd for int and nat *}
theory Parity
-imports Plain Presburger
+imports Plain "~~/src/HOL/Presburger"
begin
class even_odd = type +
--- a/src/HOL/Library/Pocklington.thy Fri Jul 04 16:33:08 2008 +0200
+++ b/src/HOL/Library/Pocklington.thy Mon Jul 07 08:47:17 2008 +0200
@@ -7,7 +7,7 @@
theory Pocklington
-imports Plain List Primes
+imports Plain "~~/src/HOL/List" "~~/src/HOL/Primes"
begin
definition modeq:: "nat => nat => nat => bool" ("(1[_ = _] '(mod _'))")
--- a/src/HOL/Library/Primes.thy Fri Jul 04 16:33:08 2008 +0200
+++ b/src/HOL/Library/Primes.thy Mon Jul 07 08:47:17 2008 +0200
@@ -7,7 +7,7 @@
header {* Primality on nat *}
theory Primes
-imports Plain ATP_Linkup GCD Parity
+imports Plain "~~/src/HOL/ATP_Linkup" GCD Parity
begin
definition
--- a/src/HOL/Library/Quotient.thy Fri Jul 04 16:33:08 2008 +0200
+++ b/src/HOL/Library/Quotient.thy Mon Jul 07 08:47:17 2008 +0200
@@ -6,7 +6,7 @@
header {* Quotient types *}
theory Quotient
-imports Plain Hilbert_Choice
+imports Plain "~~/src/HOL/Hilbert_Choice"
begin
text {*
--- a/src/HOL/Library/RType.thy Fri Jul 04 16:33:08 2008 +0200
+++ b/src/HOL/Library/RType.thy Mon Jul 07 08:47:17 2008 +0200
@@ -6,7 +6,7 @@
header {* Reflecting Pure types into HOL *}
theory RType
-imports Plain List Code_Message Code_Index (* import all 'special code' types *)
+imports Plain "~~/src/HOL/List" "~~/src/HOL/Code_Message" "~~/src/HOL/Code_Index" (* import all 'special code' types *)
begin
datatype "rtype" = RType message_string "rtype list"
--- a/src/HOL/Library/Ramsey.thy Fri Jul 04 16:33:08 2008 +0200
+++ b/src/HOL/Library/Ramsey.thy Mon Jul 07 08:47:17 2008 +0200
@@ -6,7 +6,7 @@
header "Ramsey's Theorem"
theory Ramsey
-imports Plain Presburger Infinite_Set
+imports Plain "~~/src/HOL/Presburger" Infinite_Set
begin
subsection {* Preliminaries *}
--- a/src/HOL/Library/State_Monad.thy Fri Jul 04 16:33:08 2008 +0200
+++ b/src/HOL/Library/State_Monad.thy Mon Jul 07 08:47:17 2008 +0200
@@ -3,10 +3,10 @@
Author: Florian Haftmann, TU Muenchen
*)
-header {* Combinators syntax for generic, open state monads (single threaded monads) *}
+header {* Combinator syntax for generic, open state monads (single threaded monads) *}
theory State_Monad
-imports Plain List
+imports Plain "~~/src/HOL/List"
begin
subsection {* Motivation *}
--- a/src/HOL/Library/Sublist_Order.thy Fri Jul 04 16:33:08 2008 +0200
+++ b/src/HOL/Library/Sublist_Order.thy Mon Jul 07 08:47:17 2008 +0200
@@ -7,7 +7,7 @@
header {* Sublist Ordering *}
theory Sublist_Order
-imports Plain List
+imports Plain "~~/src/HOL/List"
begin
text {*
--- a/src/HOL/Library/Univ_Poly.thy Fri Jul 04 16:33:08 2008 +0200
+++ b/src/HOL/Library/Univ_Poly.thy Mon Jul 07 08:47:17 2008 +0200
@@ -6,7 +6,7 @@
header{*Univariate Polynomials*}
theory Univ_Poly
-imports Plain "../List"
+imports Plain "~~/src/HOL/List"
begin
text{* Application of polynomial as a function. *}
--- a/src/HOL/Library/While_Combinator.thy Fri Jul 04 16:33:08 2008 +0200
+++ b/src/HOL/Library/While_Combinator.thy Mon Jul 07 08:47:17 2008 +0200
@@ -7,7 +7,7 @@
header {* A general ``while'' combinator *}
theory While_Combinator
-imports Plain Presburger
+imports Plain "~~/src/HOL/Presburger"
begin
text {*
--- a/src/HOL/Library/Word.thy Fri Jul 04 16:33:08 2008 +0200
+++ b/src/HOL/Library/Word.thy Mon Jul 07 08:47:17 2008 +0200
@@ -6,7 +6,7 @@
header {* Binary Words *}
theory Word
-imports Main
+imports "~~/src/HOL/Main"
begin
subsection {* Auxilary Lemmas *}