# HG changeset patch
# User haftmann
# Date 1215413237 -7200
# Node ID c8a6ce181805e88e692780eed600906ed885c3da
# Parent  c61507a98bff3f3c39bb57693becc18e78ffcf81
absolute imports of HOL/*.thy theories

diff -r c61507a98bff -r c8a6ce181805 src/HOL/Library/AssocList.thy
--- 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 {*
diff -r c61507a98bff -r c8a6ce181805 src/HOL/Library/BigO.thy
--- 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 {*
diff -r c61507a98bff -r c8a6ce181805 src/HOL/Library/Binomial.thy
--- 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
diff -r c61507a98bff -r c8a6ce181805 src/HOL/Library/Char_nat.thy
--- 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]. *}
diff -r c61507a98bff -r c8a6ce181805 src/HOL/Library/Code_Char.thy
--- 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]
diff -r c61507a98bff -r c8a6ce181805 src/HOL/Library/Code_Index.thy
--- 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 {*
diff -r c61507a98bff -r c8a6ce181805 src/HOL/Library/Code_Integer.thy
--- 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 {*
diff -r c61507a98bff -r c8a6ce181805 src/HOL/Library/Code_Message.thy
--- 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 *}
diff -r c61507a98bff -r c8a6ce181805 src/HOL/Library/Coinductive_List.thy
--- 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 *}
diff -r c61507a98bff -r c8a6ce181805 src/HOL/Library/Commutative_Ring.thy
--- 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
 
diff -r c61507a98bff -r c8a6ce181805 src/HOL/Library/Continuity.thy
--- 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 *}
diff -r c61507a98bff -r c8a6ce181805 src/HOL/Library/Countable.thy
--- 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 *}
diff -r c61507a98bff -r c8a6ce181805 src/HOL/Library/Dense_Linear_Order.thy
--- 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"
diff -r c61507a98bff -r c8a6ce181805 src/HOL/Library/Enum.thy
--- 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} *}
diff -r c61507a98bff -r c8a6ce181805 src/HOL/Library/Eval_Witness.thy
--- 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 {* 
diff -r c61507a98bff -r c8a6ce181805 src/HOL/Library/Executable_Set.thy
--- 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 *}
diff -r c61507a98bff -r c8a6ce181805 src/HOL/Library/FuncSet.thy
--- 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
diff -r c61507a98bff -r c8a6ce181805 src/HOL/Library/GCD.thy
--- 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 {*
diff -r c61507a98bff -r c8a6ce181805 src/HOL/Library/Heap.thy
--- 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 *}
diff -r c61507a98bff -r c8a6ce181805 src/HOL/Library/Infinite_Set.thy
--- 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
 
 
diff -r c61507a98bff -r c8a6ce181805 src/HOL/Library/LaTeXsugar.thy
--- 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 *)
diff -r c61507a98bff -r c8a6ce181805 src/HOL/Library/ListVector.thy
--- 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
diff -r c61507a98bff -r c8a6ce181805 src/HOL/Library/List_Prefix.thy
--- 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 *}
diff -r c61507a98bff -r c8a6ce181805 src/HOL/Library/List_lexord.thy
--- 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
diff -r c61507a98bff -r c8a6ce181805 src/HOL/Library/Multiset.thy
--- 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 *}
diff -r c61507a98bff -r c8a6ce181805 src/HOL/Library/NatPair.thy
--- 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{*
diff -r c61507a98bff -r c8a6ce181805 src/HOL/Library/Nat_Infinity.thy
--- 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 *}
diff -r c61507a98bff -r c8a6ce181805 src/HOL/Library/Nested_Environment.thy
--- 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 {*
diff -r c61507a98bff -r c8a6ce181805 src/HOL/Library/Numeral_Type.thy
--- 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 *}
diff -r c61507a98bff -r c8a6ce181805 src/HOL/Library/Order_Relation.thy
--- 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: *}
diff -r c61507a98bff -r c8a6ce181805 src/HOL/Library/Parity.thy
--- 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 + 
diff -r c61507a98bff -r c8a6ce181805 src/HOL/Library/Pocklington.thy
--- 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 _'))")
diff -r c61507a98bff -r c8a6ce181805 src/HOL/Library/Primes.thy
--- 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
diff -r c61507a98bff -r c8a6ce181805 src/HOL/Library/Quotient.thy
--- 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 {*
diff -r c61507a98bff -r c8a6ce181805 src/HOL/Library/RType.thy
--- 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"
diff -r c61507a98bff -r c8a6ce181805 src/HOL/Library/Ramsey.thy
--- 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 *}
diff -r c61507a98bff -r c8a6ce181805 src/HOL/Library/State_Monad.thy
--- 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 *}
diff -r c61507a98bff -r c8a6ce181805 src/HOL/Library/Sublist_Order.thy
--- 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 {*
diff -r c61507a98bff -r c8a6ce181805 src/HOL/Library/Univ_Poly.thy
--- 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. *}
diff -r c61507a98bff -r c8a6ce181805 src/HOL/Library/While_Combinator.thy
--- 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 {* 
diff -r c61507a98bff -r c8a6ce181805 src/HOL/Library/Word.thy
--- 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 *}