# HG changeset patch
# User wenzelm
# Date 1293640481 -3600
# Node ID 64cd30d6b0b8565ce2a4dffe1a027607f6c5d6e7
# Parent  35f30e07fe0d395f9df17b52ed2b6b6363215294
explicit file specifications -- avoid secondary load path;

diff -r 35f30e07fe0d -r 64cd30d6b0b8 doc-src/Classes/Thy/Setup.thy
--- a/doc-src/Classes/Thy/Setup.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/doc-src/Classes/Thy/Setup.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -1,5 +1,5 @@
 theory Setup
-imports Main Code_Integer
+imports Main "~~/src/HOL/Library/Code_Integer"
 uses
   "../../antiquote_setup.ML"
   "../../more_antiquote.ML"
diff -r 35f30e07fe0d -r 64cd30d6b0b8 doc-src/LaTeXsugar/Sugar/ROOT.ML
--- a/doc-src/LaTeXsugar/Sugar/ROOT.ML	Wed Dec 29 13:51:17 2010 +0100
+++ b/doc-src/LaTeXsugar/Sugar/ROOT.ML	Wed Dec 29 17:34:41 2010 +0100
@@ -1,4 +1,6 @@
-no_document use_thy "LaTeXsugar";
-no_document use_thy "OptionalSugar";
+no_document use_thys [
+  "~~/src/HOL/Library/LaTeXsugar",
+  "~~/src/HOL/Library/OptionalSugar"
+];
 use_thy "Sugar";
 
diff -r 35f30e07fe0d -r 64cd30d6b0b8 doc-src/LaTeXsugar/Sugar/Sugar.thy
--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -1,6 +1,6 @@
 (*<*)
 theory Sugar
-imports LaTeXsugar OptionalSugar
+imports "~~/src/HOL/Library/LaTeXsugar" "~~/src/HOL/Library/OptionalSugar"
 begin
 (*>*)
 
diff -r 35f30e07fe0d -r 64cd30d6b0b8 doc-src/TutorialI/Sets/Examples.thy
--- a/doc-src/TutorialI/Sets/Examples.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/doc-src/TutorialI/Sets/Examples.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -1,4 +1,4 @@
-theory Examples imports Main Binomial begin
+theory Examples imports Main "~~/src/HOL/Library/Binomial" begin
 
 declare [[eta_contract = false]]
 ML "Pretty.margin_default := 64"
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Algebra/Divisibility.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -5,7 +5,7 @@
 *)
 
 theory Divisibility
-imports Permutation Coset Group
+imports "~~/src/HOL/Library/Permutation" Coset Group
 begin
 
 section {* Factorial Monoids *}
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Algebra/Exponent.thy
--- a/src/HOL/Algebra/Exponent.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Algebra/Exponent.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -6,7 +6,7 @@
 *)
 
 theory Exponent
-imports Main "~~/src/HOL/Old_Number_Theory/Primes" Binomial
+imports Main "~~/src/HOL/Old_Number_Theory/Primes" "~~/src/HOL/Library/Binomial"
 begin
 
 section {*Sylow's Theorem*}
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Algebra/Group.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -5,7 +5,7 @@
 *)
 
 theory Group
-imports Lattice FuncSet
+imports Lattice "~~/src/HOL/Library/FuncSet"
 begin
 
 section {* Monoids and Groups *}
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Algebra/ROOT.ML
--- a/src/HOL/Algebra/ROOT.ML	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Algebra/ROOT.ML	Wed Dec 29 17:34:41 2010 +0100
@@ -4,7 +4,12 @@
 *)
 
 (* Preliminaries from set and number theory *)
-no_document use_thys ["FuncSet", "~~/src/HOL/Old_Number_Theory/Primes", "Binomial", "Permutation"];
+no_document use_thys [
+  "~~/src/HOL/Library/FuncSet",
+  "~~/src/HOL/Old_Number_Theory/Primes",
+  "~~/src/HOL/Library/Binomial",
+  "~~/src/HOL/Library/Permutation"
+];
 
 
 (*** New development, based on explicit structures ***)
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Auth/Guard/Guard_Shared.thy
--- a/src/HOL/Auth/Guard/Guard_Shared.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Auth/Guard/Guard_Shared.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -11,7 +11,7 @@
 
 header{*lemmas on guarded messages for protocols with symmetric keys*}
 
-theory Guard_Shared imports Guard GuardK Shared begin
+theory Guard_Shared imports Guard GuardK "../Shared" begin
 
 subsection{*Extensions to Theory @{text Shared}*}
 
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Auth/ROOT.ML
--- a/src/HOL/Auth/ROOT.ML	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Auth/ROOT.ML	Wed Dec 29 17:34:41 2010 +0100
@@ -1,2 +1,7 @@
-
-use_thys ["Auth_Shared", "Auth_Public", "Smartcard/Auth_Smartcard", "Guard/Auth_Guard_Shared", "Guard/Auth_Guard_Public"];
+use_thys [
+  "Auth_Shared",
+  "Auth_Public",
+  "Smartcard/Auth_Smartcard",
+  "Guard/Auth_Guard_Shared",
+  "Guard/Auth_Guard_Public"
+];
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Auth/Smartcard/Smartcard.thy
--- a/src/HOL/Auth/Smartcard/Smartcard.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Auth/Smartcard/Smartcard.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -4,7 +4,7 @@
 header{*Theory of smartcards*}
 
 theory Smartcard
-imports EventSC All_Symmetric
+imports EventSC "../All_Symmetric"
 begin
 
 text{*  
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Auth/TLS.thy
--- a/src/HOL/Auth/TLS.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Auth/TLS.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -40,7 +40,7 @@
 
 header{*The TLS Protocol: Transport Layer Security*}
 
-theory TLS imports Public Nat_Bijection begin
+theory TLS imports Public "~~/src/HOL/Library/Nat_Bijection" begin
 
 definition certificate :: "[agent,key] => msg" where
     "certificate A KA == Crypt (priSK Server) {|Agent A, Key KA|}"
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -4,7 +4,12 @@
 header {* Prove Real Valued Inequalities by Computation *}
 
 theory Approximation
-imports Complex_Main Float Reflection "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Efficient_Nat
+imports
+  Complex_Main
+  "~~/src/HOL/Library/Float"
+  "~~/src/HOL/Library/Reflection"
+  "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
+  "~~/src/HOL/Library/Efficient_Nat"
 begin
 
 section "Horner Scheme"
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Decision_Procs/Cooper.thy
--- a/src/HOL/Decision_Procs/Cooper.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Decision_Procs/Cooper.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -3,7 +3,7 @@
 *)
 
 theory Cooper
-imports Complex_Main Efficient_Nat
+imports Complex_Main "~~/src/HOL/Library/Efficient_Nat"
 uses ("cooper_tac.ML")
 begin
 
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Decision_Procs/Ferrack.thy
--- a/src/HOL/Decision_Procs/Ferrack.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Decision_Procs/Ferrack.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -3,7 +3,7 @@
 *)
 
 theory Ferrack
-imports Complex_Main Dense_Linear_Order Efficient_Nat
+imports Complex_Main Dense_Linear_Order "~~/src/HOL/Library/Efficient_Nat"
 uses ("ferrack_tac.ML")
 begin
 
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -3,7 +3,7 @@
 *)
 
 theory MIR
-imports Complex_Main Dense_Linear_Order Efficient_Nat
+imports Complex_Main Dense_Linear_Order "~~/src/HOL/Library/Efficient_Nat"
 uses ("mir_tac.ML")
 begin
 
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -5,9 +5,10 @@
 header{* A formalization of Ferrante and Rackoff's procedure with polynomial parameters, see Paper in CALCULEMUS 2008 *}
 
 theory Parametric_Ferrante_Rackoff
-imports Reflected_Multivariate_Polynomial
+imports
+  Reflected_Multivariate_Polynomial
   Dense_Linear_Order
-  Efficient_Nat
+  "~~/src/HOL/Library/Efficient_Nat"
 begin
 
 subsection {* Terms *}
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -5,7 +5,7 @@
 header {* Implementation and verification of multivariate polynomials *}
 
 theory Reflected_Multivariate_Polynomial
-imports Complex_Main Abstract_Rat Polynomial_List
+imports Complex_Main "~~/src/HOL/Library/Abstract_Rat" Polynomial_List
 begin
 
   (* Implementation *)
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/HOLCF/Bifinite.thy
--- a/src/HOL/HOLCF/Bifinite.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/HOLCF/Bifinite.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -5,7 +5,7 @@
 header {* Profinite and bifinite cpos *}
 
 theory Bifinite
-imports Map_Functions Countable
+imports Map_Functions "~~/src/HOL/Library/Countable"
 begin
 
 default_sort cpo
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/HOLCF/FOCUS/Fstream.thy
--- a/src/HOL/HOLCF/FOCUS/Fstream.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/HOLCF/FOCUS/Fstream.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -9,7 +9,7 @@
 header {* FOCUS flat streams *}
 
 theory Fstream
-imports Stream
+imports "~~/src/HOL/HOLCF/Library/Stream"
 begin
 
 default_sort type
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/HOLCF/FOCUS/Fstreams.thy
--- a/src/HOL/HOLCF/FOCUS/Fstreams.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/HOLCF/FOCUS/Fstreams.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -7,7 +7,7 @@
 *)
 
 theory Fstreams
-imports Stream
+imports "~~/src/HOL/HOLCF/Library/Stream"
 begin
 
 default_sort type
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/HOLCF/FOCUS/Stream_adm.thy
--- a/src/HOL/HOLCF/FOCUS/Stream_adm.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/HOLCF/FOCUS/Stream_adm.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -5,7 +5,7 @@
 header {* Admissibility for streams *}
 
 theory Stream_adm
-imports Stream Continuity
+imports "~~/src/HOL/HOLCF/Library/Stream" "~~/src/HOL/Library/Continuity"
 begin
 
 definition
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/HOLCF/Library/Stream.thy
--- a/src/HOL/HOLCF/Library/Stream.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/HOLCF/Library/Stream.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -5,7 +5,7 @@
 header {* General Stream domain *}
 
 theory Stream
-imports HOLCF Nat_Infinity
+imports HOLCF "~~/src/HOL/Library/Nat_Infinity"
 begin
 
 default_sort pcpo
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/HOLCF/ROOT.ML
--- a/src/HOL/HOLCF/ROOT.ML	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/HOLCF/ROOT.ML	Wed Dec 29 17:34:41 2010 +0100
@@ -4,6 +4,6 @@
 HOLCF -- a semantic extension of HOL by the LCF logic.
 *)
 
-no_document use_thys ["Nat_Bijection", "Countable"];
+no_document use_thys ["~~/src/HOL/Library/Nat_Bijection", "~~/src/HOL/Library/Countable"];
 
 use_thys ["Plain_HOLCF", "Fixrec", "HOLCF"];
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/HOLCF/Universal.thy
--- a/src/HOL/HOLCF/Universal.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/HOLCF/Universal.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -5,7 +5,7 @@
 header {* A universal bifinite domain *}
 
 theory Universal
-imports Bifinite Completion Nat_Bijection
+imports Bifinite Completion "~~/src/HOL/Library/Nat_Bijection"
 begin
 
 subsection {* Basis for universal domain *}
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/HOLCF/ex/Dagstuhl.thy
--- a/src/HOL/HOLCF/ex/Dagstuhl.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/HOLCF/ex/Dagstuhl.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -1,5 +1,5 @@
 theory Dagstuhl
-imports Stream
+imports "~~/src/HOL/HOLCF/Library/Stream"
 begin
 
 axiomatization
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/HOLCF/ex/Focus_ex.thy
--- a/src/HOL/HOLCF/ex/Focus_ex.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/HOLCF/ex/Focus_ex.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -99,7 +99,7 @@
 *)
 
 theory Focus_ex
-imports Stream
+imports "~~/src/HOL/HOLCF/Library/Stream"
 begin
 
 typedecl ('a, 'b) tc
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Hahn_Banach/Bounds.thy
--- a/src/HOL/Hahn_Banach/Bounds.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Hahn_Banach/Bounds.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -5,7 +5,7 @@
 header {* Bounds *}
 
 theory Bounds
-imports Main ContNotDenum
+imports Main "~~/src/HOL/Library/ContNotDenum"
 begin
 
 locale lub =
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Hahn_Banach/Vector_Space.thy
--- a/src/HOL/Hahn_Banach/Vector_Space.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Hahn_Banach/Vector_Space.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -5,7 +5,7 @@
 header {* Vector spaces *}
 
 theory Vector_Space
-imports Real Bounds Zorn
+imports Real Bounds "~~/src/HOL/Library/Zorn"
 begin
 
 subsection {* Signature *}
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Imperative_HOL/Heap.thy
--- a/src/HOL/Imperative_HOL/Heap.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Imperative_HOL/Heap.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -5,7 +5,7 @@
 header {* A polymorphic heap based on cantor encodings *}
 
 theory Heap
-imports Main Countable
+imports Main "~~/src/HOL/Library/Countable"
 begin
 
 subsection {* Representable types *}
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -5,7 +5,10 @@
 header {* A monad with a polymorphic heap and primitive reasoning infrastructure *}
 
 theory Heap_Monad
-imports Heap Monad_Syntax Code_Natural
+imports
+  Heap
+  "~~/src/HOL/Library/Monad_Syntax"
+  "~~/src/HOL/Library/Code_Natural"
 begin
 
 subsection {* The monad *}
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Imperative_HOL/Overview.thy
--- a/src/HOL/Imperative_HOL/Overview.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Imperative_HOL/Overview.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -4,7 +4,7 @@
 
 (*<*)
 theory Overview
-imports Imperative_HOL LaTeXsugar
+imports Imperative_HOL "~~/src/HOL/Library/LaTeXsugar"
 begin
 
 (* type constraints with spacing *)
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Imperative_HOL/ROOT.ML
--- a/src/HOL/Imperative_HOL/ROOT.ML	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Imperative_HOL/ROOT.ML	Wed Dec 29 17:34:41 2010 +0100
@@ -1,4 +1,7 @@
-
-no_document use_thys ["Countable", "Monad_Syntax", "Code_Natural", "LaTeXsugar"];
+no_document use_thys [
+  "~~/src/HOL/Library/Countable",
+  "~~/src/HOL/Library/Monad_Syntax",
+  "~~/src/HOL/Library/Code_Natural",
+  "~~/src/HOL/Library/LaTeXsugar"];
 
 use_thys ["Imperative_HOL_ex"];
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -5,7 +5,11 @@
 header {* An imperative implementation of Quicksort on arrays *}
 
 theory Imperative_Quicksort
-imports Imperative_HOL Subarray Multiset Efficient_Nat
+imports
+  Imperative_HOL
+  Subarray
+  "~~/src/HOL/Library/Multiset"
+  "~~/src/HOL/Library/Efficient_Nat"
 begin
 
 text {* We prove QuickSort correct in the Relational Calculus. *}
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Imperative_HOL/ex/SatChecker.thy
--- a/src/HOL/Imperative_HOL/ex/SatChecker.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -5,7 +5,7 @@
 header {* An efficient checker for proofs from a SAT solver *}
 
 theory SatChecker
-imports RBT_Impl Sorted_List Imperative_HOL
+imports "~~/src/HOL/Library/RBT_Impl" Sorted_List Imperative_HOL
 begin
 
 section{* General settings and functions for our representation of clauses *}
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Imperative_HOL/ex/Sublist.thy
--- a/src/HOL/Imperative_HOL/ex/Sublist.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Imperative_HOL/ex/Sublist.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -5,7 +5,7 @@
 header {* Slices of lists *}
 
 theory Sublist
-imports Multiset
+imports "~~/src/HOL/Library/Multiset"
 begin
 
 lemma sublist_split: "i \<le> j \<and> j \<le> k \<Longrightarrow> sublist xs {i..<j} @ sublist xs {j..<k} = sublist xs {i..<k}" 
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Import/HOL4Compat.thy
--- a/src/HOL/Import/HOL4Compat.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Import/HOL4Compat.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -3,7 +3,11 @@
 *)
 
 theory HOL4Compat
-imports HOL4Setup Complex_Main "~~/src/HOL/Old_Number_Theory/Primes" ContNotDenum
+imports
+  HOL4Setup
+  Complex_Main
+  "~~/src/HOL/Old_Number_Theory/Primes"
+  "~~/src/HOL/Library/ContNotDenum"
 begin
 
 abbreviation (input) mem (infixl "mem" 55) where "x mem xs \<equiv> List.member xs x"
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/IsaMakefile	Wed Dec 29 17:34:41 2010 +0100
@@ -1524,7 +1524,7 @@
 
 HOLCF-FOCUS: HOLCF $(LOG)/HOLCF-FOCUS.gz
 
-$(LOG)/HOLCF-FOCUS.gz: $(OUT)/HOLCF \
+$(LOG)/HOLCF-FOCUS.gz: $(OUT)/HOLCF HOLCF/FOCUS/ROOT.ML \
   HOLCF/Library/Stream.thy \
   HOLCF/FOCUS/Fstreams.thy \
   HOLCF/FOCUS/Fstream.thy \
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Isar_Examples/Knaster_Tarski.thy
--- a/src/HOL/Isar_Examples/Knaster_Tarski.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Isar_Examples/Knaster_Tarski.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -7,7 +7,7 @@
 header {* Textbook-style reasoning: the Knaster-Tarski Theorem *}
 
 theory Knaster_Tarski
-imports Main Lattice_Syntax
+imports Main "~~/src/HOL/Library/Lattice_Syntax"
 begin
 
 
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Matrix/ComputeFloat.thy
--- a/src/HOL/Matrix/ComputeFloat.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Matrix/ComputeFloat.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -5,7 +5,7 @@
 header {* Floating Point Representation of the Reals *}
 
 theory ComputeFloat
-imports Complex_Main Lattice_Algebras
+imports Complex_Main "~~/src/HOL/Library/Lattice_Algebras"
 uses "~~/src/Tools/float.ML" ("~~/src/HOL/Tools/float_arith.ML")
 begin
 
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Matrix/LP.thy
--- a/src/HOL/Matrix/LP.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Matrix/LP.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -3,7 +3,7 @@
 *)
 
 theory LP 
-imports Main Lattice_Algebras
+imports Main "~~/src/HOL/Library/Lattice_Algebras"
 begin
 
 lemma le_add_right_mono: 
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Matrix/Matrix.thy
--- a/src/HOL/Matrix/Matrix.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Matrix/Matrix.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -3,7 +3,7 @@
 *)
 
 theory Matrix
-imports Main Lattice_Algebras
+imports Main "~~/src/HOL/Library/Lattice_Algebras"
 begin
 
 types 'a infmatrix = "nat \<Rightarrow> nat \<Rightarrow> 'a"
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Metis_Examples/Abstraction.thy
--- a/src/HOL/Metis_Examples/Abstraction.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Metis_Examples/Abstraction.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -6,7 +6,7 @@
 *)
 
 theory Abstraction
-imports Main FuncSet
+imports Main "~~/src/HOL/Library/FuncSet"
 begin
 
 (*For Christoph Benzmueller*)
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Metis_Examples/BigO.thy
--- a/src/HOL/Metis_Examples/BigO.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Metis_Examples/BigO.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -8,7 +8,11 @@
 header {* Big O notation *}
 
 theory BigO
-imports "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Main Function_Algebras Set_Algebras
+imports
+  "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
+  Main
+  "~~/src/HOL/Library/Function_Algebras"
+  "~~/src/HOL/Library/Set_Algebras"
 begin
 
 subsection {* Definitions *}
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Metis_Examples/Tarski.thy
--- a/src/HOL/Metis_Examples/Tarski.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Metis_Examples/Tarski.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -8,7 +8,7 @@
 header {* The Full Theorem of Tarski *}
 
 theory Tarski
-imports Main FuncSet
+imports Main "~~/src/HOL/Library/FuncSet"
 begin
 
 (*Many of these higher-order problems appear to be impossible using the
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/MicroJava/BV/BVExample.thy
--- a/src/HOL/MicroJava/BV/BVExample.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -5,7 +5,11 @@
 header {* \isaheader{Example Welltypings}\label{sec:BVExample} *}
 
 theory BVExample
-imports "../JVM/JVMListExample" BVSpecTypeSafe JVM Executable_Set
+imports
+  "../JVM/JVMListExample"
+  BVSpecTypeSafe
+  JVM
+  "~~/src/HOL/Library/Executable_Set"
 begin
 
 text {*
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/MicroJava/DFA/Kildall.thy
--- a/src/HOL/MicroJava/DFA/Kildall.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/MicroJava/DFA/Kildall.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -6,7 +6,7 @@
 header {* \isaheader{Kildall's Algorithm}\label{sec:Kildall} *}
 
 theory Kildall
-imports SemilatAlg While_Combinator
+imports SemilatAlg "~~/src/HOL/Library/While_Combinator"
 begin
 
 primrec propa :: "'s binop \<Rightarrow> (nat \<times> 's) list \<Rightarrow> 's list \<Rightarrow> nat set \<Rightarrow> 's list * nat set" where
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/MicroJava/DFA/Semilat.thy
--- a/src/HOL/MicroJava/DFA/Semilat.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/MicroJava/DFA/Semilat.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -9,7 +9,7 @@
 *}
 
 theory Semilat
-imports Main While_Combinator
+imports Main "~~/src/HOL/Library/While_Combinator"
 begin
 
 types 
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/MicroJava/ROOT.ML
--- a/src/HOL/MicroJava/ROOT.ML	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/MicroJava/ROOT.ML	Wed Dec 29 17:34:41 2010 +0100
@@ -1,3 +1,3 @@
-no_document use_thys ["While_Combinator"];
+no_document use_thys ["~~/src/HOL/Library/While_Combinator"];
 
 use_thys ["MicroJava"];
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -6,7 +6,7 @@
 header {* Convex sets, functions and related things. *}
 
 theory Convex_Euclidean_Space
-imports Topology_Euclidean_Space Convex Set_Algebras
+imports Topology_Euclidean_Space Convex "~~/src/HOL/Library/Set_Algebras"
 begin
 
 
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -6,8 +6,12 @@
 
 theory Euclidean_Space
 imports
-  Complex_Main "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
-  Infinite_Set Inner_Product L2_Norm Convex
+  Complex_Main
+  "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
+  "~~/src/HOL/Library/Infinite_Set"
+  "~~/src/HOL/Library/Inner_Product"
+  L2_Norm
+  "~~/src/HOL/Library/Convex"
 uses
   "~~/src/HOL/Library/positivstellensatz.ML"  (* FIXME duplicate use!? *)
   ("normarith.ML")
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -5,7 +5,10 @@
 header {* Definition of finite Cartesian product types. *}
 
 theory Finite_Cartesian_Product
-imports Inner_Product L2_Norm Numeral_Type
+imports
+  "~~/src/HOL/Library/Inner_Product"
+  L2_Norm
+  "~~/src/HOL/Library/Numeral_Type"
 begin
 
 subsection {* Finite Cartesian products, with indexing and lambdas. *}
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -4,7 +4,10 @@
     Translation from HOL light: Robert Himmelmann, TU Muenchen *)
 
 theory Integration
-  imports Derivative "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Indicator_Function
+imports
+  Derivative
+  "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
+  "~~/src/HOL/Library/Indicator_Function"
 begin
 
 declare [[smt_certificates="Integration.certs"]]
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -6,7 +6,7 @@
 header {* Elementary topology in Euclidean space. *}
 
 theory Topology_Euclidean_Space
-imports SEQ Euclidean_Space Glbs
+imports SEQ Euclidean_Space "~~/src/HOL/Library/Glbs"
 begin
 
 (* to be moved elsewhere *)
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/NSA/NSComplex.thy
--- a/src/HOL/NSA/NSComplex.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/NSA/NSComplex.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -7,7 +7,7 @@
 header{*Nonstandard Complex Numbers*}
 
 theory NSComplex
-imports Complex "../Hyperreal/NSA"
+imports Complex NSA
 begin
 
 types hcomplex = "complex star"
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Nitpick_Examples/Manual_Nits.thy
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -12,7 +12,7 @@
    suite. *)
 
 theory Manual_Nits
-imports Main Quotient_Product RealDef
+imports Main "~~/src/HOL/Library/Quotient_Product" RealDef
 begin
 
 chapter {* 3. First Steps *}
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -1,5 +1,5 @@
 theory Nominal 
-imports Main Infinite_Set
+imports Main "~~/src/HOL/Library/Infinite_Set"
 uses
   ("nominal_thmdecls.ML")
   ("nominal_atoms.ML")
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Nominal/ROOT.ML
--- a/src/HOL/Nominal/ROOT.ML	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Nominal/ROOT.ML	Wed Dec 29 17:34:41 2010 +0100
@@ -4,5 +4,5 @@
 The nominal datatype package.
 *)
 
-no_document use_thys ["Infinite_Set"];
+no_document use_thys ["~~/src/HOL/Library/Infinite_Set"];
 use_thys ["Nominal"];
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Number_Theory/UniqueFactorization.thy
--- a/src/HOL/Number_Theory/UniqueFactorization.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -12,7 +12,7 @@
 header {* UniqueFactorization *}
 
 theory UniqueFactorization
-imports Cong Multiset
+imports Cong "~~/src/HOL/Library/Multiset"
 begin
 
 (* inherited from Multiset *)
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Old_Number_Theory/Factorization.thy
--- a/src/HOL/Old_Number_Theory/Factorization.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Old_Number_Theory/Factorization.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -6,7 +6,7 @@
 header {* Fundamental Theorem of Arithmetic (unique factorization into primes) *}
 
 theory Factorization
-imports Primes Permutation
+imports Primes "~~/src/HOL/Library/Permutation"
 begin
 
 
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Old_Number_Theory/Finite2.thy
--- a/src/HOL/Old_Number_Theory/Finite2.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Old_Number_Theory/Finite2.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -5,7 +5,7 @@
 header {*Finite Sets and Finite Sums*}
 
 theory Finite2
-imports IntFact Infinite_Set
+imports IntFact "~~/src/HOL/Library/Infinite_Set"
 begin
 
 text{*
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Old_Number_Theory/ROOT.ML
--- a/src/HOL/Old_Number_Theory/ROOT.ML	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Old_Number_Theory/ROOT.ML	Wed Dec 29 17:34:41 2010 +0100
@@ -1,4 +1,15 @@
+no_document use_thys [
+  "~~/src/HOL/Library/Infinite_Set",
+  "~~/src/HOL/Library/Permutation"
+];
 
-no_document use_thys ["Infinite_Set", "Permutation"];
-use_thys ["Fib", "Factorization", "Chinese", "WilsonRuss",
-  "WilsonBij", "Quadratic_Reciprocity", "Primes", "Pocklington"];
+use_thys [
+  "Fib",
+  "Factorization",
+  "Chinese",
+  "WilsonRuss",
+  "WilsonBij",
+  "Quadratic_Reciprocity",
+  "Primes",
+  "Pocklington"
+];
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Predicate_Compile_Examples/Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Examples.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Examples.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -1,5 +1,5 @@
 theory Examples
-imports Main Predicate_Compile_Alternative_Defs
+imports Main "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs"
 begin
 
 section {* Formal Languages *}
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -1,5 +1,5 @@
 theory Hotel_Example_Prolog
-imports Hotel_Example Predicate_Compile_Alternative_Defs Code_Prolog
+imports Hotel_Example "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs" Code_Prolog
 begin
 
 declare Let_def[code_pred_inline]
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -1,5 +1,5 @@
 theory Hotel_Example_Small_Generator
-imports Hotel_Example Predicate_Compile_Alternative_Defs
+imports Hotel_Example "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs"
 uses "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML"
 begin
 
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Predicate_Compile_Examples/IMP_1.thy
--- a/src/HOL/Predicate_Compile_Examples/IMP_1.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/IMP_1.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -1,5 +1,5 @@
 theory IMP_1
-imports "Predicate_Compile_Quickcheck"
+imports "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
 begin
 
 subsection {* IMP *}
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Predicate_Compile_Examples/IMP_2.thy
--- a/src/HOL/Predicate_Compile_Examples/IMP_2.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/IMP_2.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -1,5 +1,5 @@
 theory IMP_2
-imports "Predicate_Compile_Quickcheck"
+imports "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
 begin
 
 subsection {* IMP *}
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Predicate_Compile_Examples/IMP_3.thy
--- a/src/HOL/Predicate_Compile_Examples/IMP_3.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/IMP_3.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -1,5 +1,5 @@
 theory IMP_3
-imports "Predicate_Compile_Quickcheck"
+imports "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
 begin
 
 subsection {* IMP *}
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Predicate_Compile_Examples/IMP_4.thy
--- a/src/HOL/Predicate_Compile_Examples/IMP_4.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/IMP_4.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -1,5 +1,5 @@
 theory IMP_4
-imports Predicate_Compile_Quickcheck
+imports "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
 begin
 
 subsection {* IMP *}
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Predicate_Compile_Examples/List_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/List_Examples.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/List_Examples.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -1,5 +1,5 @@
 theory List_Examples
-imports Main "Predicate_Compile_Quickcheck" "Code_Prolog"
+imports Main "~~/src/HOL/Library/Predicate_Compile_Quickcheck" "Code_Prolog"
 begin
 
 setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *}
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -1,5 +1,5 @@
 theory Predicate_Compile_Quickcheck_Examples
-imports Predicate_Compile_Quickcheck
+imports "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
 begin
 
 section {* Sets *}
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -1,5 +1,5 @@
 theory Predicate_Compile_Tests
-imports Predicate_Compile_Alternative_Defs
+imports "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs"
 begin
 
 subsection {* Basic predicates *}
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy
--- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -1,5 +1,5 @@
 theory Reg_Exp_Example
-imports Predicate_Compile_Quickcheck Code_Prolog
+imports "~~/src/HOL/Library/Predicate_Compile_Quickcheck" Code_Prolog
 begin
 
 text {* An example from the experiments from SmallCheck (http://www.cs.york.ac.uk/fp/smallcheck/) *}
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -1,5 +1,5 @@
 theory Specialisation_Examples
-imports Main Predicate_Compile_Alternative_Defs
+imports Main "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs"
 begin
 
 section {* Specialisation Examples *}
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Probability/Information.thy
--- a/src/HOL/Probability/Information.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Probability/Information.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -1,5 +1,8 @@
 theory Information
-imports Probability_Space Convex Lebesgue_Measure
+imports
+  Probability_Space
+  "~~/src/HOL/Library/Convex"
+  Lebesgue_Measure
 begin
 
 lemma log_le: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> x \<le> y \<Longrightarrow> log a x \<le> log a y"
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Probability/Positive_Extended_Real.thy
--- a/src/HOL/Probability/Positive_Extended_Real.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Probability/Positive_Extended_Real.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -3,7 +3,7 @@
 header {* A type for positive real numbers with infinity *}
 
 theory Positive_Extended_Real
-  imports Complex_Main Nat_Bijection Multivariate_Analysis
+  imports Complex_Main "~~/src/HOL/Library/Nat_Bijection" Multivariate_Analysis
 begin
 
 lemma (in complete_lattice) Sup_start:
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -6,7 +6,13 @@
 
 header {* Sigma Algebras *}
 
-theory Sigma_Algebra imports Main Countable FuncSet Indicator_Function begin
+theory Sigma_Algebra
+imports
+  Main
+  "~~/src/HOL/Library/Countable"
+  "~~/src/HOL/Library/FuncSet"
+  "~~/src/HOL/Library/Indicator_Function"
+begin
 
 text {* Sigma algebras are an elementary concept in measure
   theory. To measure --- that is to integrate --- functions, we first have
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy
--- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -3,7 +3,7 @@
 header {* Formalization of a Countermeasure by Koepf & Duermuth 2009 *}
 
 theory Koepf_Duermuth_Countermeasure
-  imports Information Permutation
+  imports Information "~~/src/HOL/Library/Permutation"
 begin
 
 lemma
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Proofs/Extraction/Euclid.thy
--- a/src/HOL/Proofs/Extraction/Euclid.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Proofs/Extraction/Euclid.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -7,7 +7,10 @@
 header {* Euclid's theorem *}
 
 theory Euclid
-imports "~~/src/HOL/Number_Theory/UniqueFactorization" Util Efficient_Nat
+imports
+  "~~/src/HOL/Number_Theory/UniqueFactorization"
+  Util
+  "~~/src/HOL/Library/Efficient_Nat"
 begin
 
 text {*
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Proofs/Extraction/Higman.thy
--- a/src/HOL/Proofs/Extraction/Higman.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Proofs/Extraction/Higman.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -6,7 +6,7 @@
 header {* Higman's lemma *}
 
 theory Higman
-imports Main State_Monad Random
+imports Main "~~/src/HOL/Library/State_Monad" Random
 begin
 
 text {*
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Proofs/Extraction/Pigeonhole.thy
--- a/src/HOL/Proofs/Extraction/Pigeonhole.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Proofs/Extraction/Pigeonhole.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -5,7 +5,7 @@
 header {* The pigeonhole principle *}
 
 theory Pigeonhole
-imports Util Efficient_Nat
+imports Util "~~/src/HOL/Library/Efficient_Nat"
 begin
 
 text {*
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Proofs/Extraction/ROOT.ML
--- a/src/HOL/Proofs/Extraction/ROOT.ML	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Proofs/Extraction/ROOT.ML	Wed Dec 29 17:34:41 2010 +0100
@@ -1,6 +1,12 @@
 (* Examples for program extraction in Higher-Order Logic *)
 
-no_document use_thys ["Efficient_Nat", "Monad_Syntax", "~~/src/HOL/Number_Theory/Primes"];
+no_document use_thys [
+  "~~/src/HOL/Library/Efficient_Nat",
+  "~~/src/HOL/Library/Monad_Syntax",
+  "~~/src/HOL/Number_Theory/Primes"
+];
+
 share_common_data ();
+
 no_document use_thys ["~~/src/HOL/Number_Theory/UniqueFactorization"];
 use_thys ["Greatest_Common_Divisor", "Warshall", "Higman", "Pigeonhole", "Euclid"];
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Proofs/Lambda/ROOT.ML
--- a/src/HOL/Proofs/Lambda/ROOT.ML	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Proofs/Lambda/ROOT.ML	Wed Dec 29 17:34:41 2010 +0100
@@ -1,2 +1,2 @@
-no_document use_thys ["Code_Integer"];
+no_document use_thys ["~~/src/HOL/Library/Code_Integer"];
 use_thys ["Eta", "StrongNorm", "Standardization", "WeakNorm"];
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Proofs/Lambda/WeakNorm.thy
--- a/src/HOL/Proofs/Lambda/WeakNorm.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Proofs/Lambda/WeakNorm.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -6,7 +6,7 @@
 header {* Weak normalization for simply-typed lambda calculus *}
 
 theory WeakNorm
-imports Type NormalForm Code_Integer
+imports Type NormalForm "~~/src/HOL/Library/Code_Integer"
 begin
 
 text {*
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Quotient_Examples/FSet.thy
--- a/src/HOL/Quotient_Examples/FSet.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Quotient_Examples/FSet.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -6,7 +6,7 @@
 *)
 
 theory FSet
-imports Quotient_List More_List
+imports "~~/src/HOL/Library/Quotient_List" "~~/src/HOL/Library/More_List"
 begin
 
 text {* 
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Quotient_Examples/Quotient_Int.thy
--- a/src/HOL/Quotient_Examples/Quotient_Int.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_Int.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -5,7 +5,7 @@
 Integers based on Quotients, based on an older version by Larry Paulson.
 *)
 theory Quotient_Int
-imports Quotient_Product Nat
+imports "~~/src/HOL/Library/Quotient_Product" Nat
 begin
 
 fun
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/SET_Protocol/Message_SET.thy
--- a/src/HOL/SET_Protocol/Message_SET.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/SET_Protocol/Message_SET.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -7,7 +7,7 @@
 header{*The Message Theory, Modified for SET*}
 
 theory Message_SET
-imports Main Nat_Bijection
+imports Main "~~/src/HOL/Library/Nat_Bijection"
 begin
 
 subsection{*General Lemmas*}
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/SET_Protocol/ROOT.ML
--- a/src/HOL/SET_Protocol/ROOT.ML	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/SET_Protocol/ROOT.ML	Wed Dec 29 17:34:41 2010 +0100
@@ -1,3 +1,2 @@
-
-no_document use_thys ["Nat_Bijection"];
+no_document use_thys ["~~/src/HOL/Library/Nat_Bijection"];
 use_thys ["SET_Protocol"];
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/UNITY/Follows.thy
--- a/src/HOL/UNITY/Follows.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/UNITY/Follows.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -5,7 +5,9 @@
 
 header{*The Follows Relation of Charpentier and Sivilotte*}
 
-theory Follows imports SubstAx ListOrder Multiset begin
+theory Follows
+imports SubstAx ListOrder "~~/src/HOL/Library/Multiset"
+begin
 
 definition Follows :: "['a => 'b::{order}, 'a => 'b::{order}] => 'a program set" (infixl "Fols" 65) where
    "f Fols g == Increasing g \<inter> Increasing f Int
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Unix/Unix.thy
--- a/src/HOL/Unix/Unix.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Unix/Unix.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -5,7 +5,10 @@
 header {* Unix file-systems \label{sec:unix-file-system} *}
 
 theory Unix
-imports Main Nested_Environment List_Prefix
+imports
+  Main
+  "~~/src/HOL/Library/Nested_Environment"
+  "~~/src/HOL/Library/List_Prefix"
 begin
 
 text {*
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Word/Bit_Operations.thy
--- a/src/HOL/Word/Bit_Operations.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Word/Bit_Operations.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -5,7 +5,7 @@
 header {* Syntactic classes for bitwise operations *}
 
 theory Bit_Operations
-imports Bit
+imports "~~/src/HOL/Library/Bit"
 begin
 
 class bit =
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Word/Bit_Representation.thy
--- a/src/HOL/Word/Bit_Representation.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Word/Bit_Representation.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -8,7 +8,7 @@
 header {* Basic Definitions for Binary Integers *}
 
 theory Bit_Representation
-imports Misc_Numeric Bit
+imports Misc_Numeric "~~/src/HOL/Library/Bit"
 begin
 
 subsection {* Further properties of numerals *}
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Word/Type_Length.thy
--- a/src/HOL/Word/Type_Length.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Word/Type_Length.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -5,7 +5,7 @@
 header {* Assigning lengths to types by typeclasses *}
 
 theory Type_Length
-imports Numeral_Type
+imports "~~/src/HOL/Library/Numeral_Type"
 begin
 
 text {*
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/Word/Word.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -5,7 +5,11 @@
 header {* A type of finite bit strings *}
 
 theory Word
-imports Type_Length Misc_Typedef Boolean_Algebra Bool_List_Representation
+imports
+  Type_Length
+  Misc_Typedef
+  "~~/src/HOL/Library/Boolean_Algebra"
+  Bool_List_Representation
 uses ("~~/src/HOL/Word/Tools/smt_word.ML")
 begin
 
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/ZF/LProd.thy
--- a/src/HOL/ZF/LProd.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/ZF/LProd.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -6,7 +6,7 @@
 *)
 
 theory LProd 
-imports Multiset
+imports "~~/src/HOL/Library/Multiset"
 begin
 
 inductive_set
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/ex/Efficient_Nat_examples.thy
--- a/src/HOL/ex/Efficient_Nat_examples.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/ex/Efficient_Nat_examples.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -5,7 +5,7 @@
 header {* Simple examples for Efficient\_Nat theory. *}
 
 theory Efficient_Nat_examples
-imports Complex_Main Efficient_Nat
+imports Complex_Main "~~/src/HOL/Library/Efficient_Nat"
 begin
 
 fun to_n :: "nat \<Rightarrow> nat list" where
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/ex/Execute_Choice.thy
--- a/src/HOL/ex/Execute_Choice.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/ex/Execute_Choice.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -3,7 +3,7 @@
 header {* A simple cookbook example how to eliminate choice in programs. *}
 
 theory Execute_Choice
-imports Main AssocList
+imports Main "~~/src/HOL/Library/AssocList"
 begin
 
 text {*
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/ex/Fundefs.thy
--- a/src/HOL/ex/Fundefs.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/ex/Fundefs.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -5,7 +5,7 @@
 header {* Examples of function definitions *}
 
 theory Fundefs 
-imports Parity Monad_Syntax
+imports Parity "~~/src/HOL/Library/Monad_Syntax"
 begin
 
 subsection {* Very basic *}
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/ex/Landau.thy
--- a/src/HOL/ex/Landau.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/ex/Landau.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -4,7 +4,7 @@
 header {* Comparing growth of functions on natural numbers by a preorder relation *}
 
 theory Landau
-imports Main Preorder
+imports Main "~~/src/HOL/Library/Preorder"
 begin
 
 text {*
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/ex/MergeSort.thy
--- a/src/HOL/ex/MergeSort.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/ex/MergeSort.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -6,7 +6,7 @@
 header{*Merge Sort*}
 
 theory MergeSort
-imports Multiset
+imports "~~/src/HOL/Library/Multiset"
 begin
 
 context linorder
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/ex/Quickcheck_Lattice_Examples.thy
--- a/src/HOL/ex/Quickcheck_Lattice_Examples.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/ex/Quickcheck_Lattice_Examples.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -4,7 +4,7 @@
 *)
 
 theory Quickcheck_Lattice_Examples
-imports Quickcheck_Types
+imports "~~/src/HOL/Library/Quickcheck_Types"
 begin
 
 text {* We show how other default types help to find counterexamples to propositions if
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/ex/Quicksort.thy
--- a/src/HOL/ex/Quicksort.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/ex/Quicksort.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -5,7 +5,7 @@
 header {* Quicksort with function package *}
 
 theory Quicksort
-imports Main Multiset
+imports Main "~~/src/HOL/Library/Multiset"
 begin
 
 context linorder
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/ex/ROOT.ML	Wed Dec 29 17:34:41 2010 +0100
@@ -4,9 +4,9 @@
 *)
 
 no_document use_thys [
-  "State_Monad",
+  "~~/src/HOL/Library/State_Monad",
   "Efficient_Nat_examples",
-  "FuncSet",
+  "~~/src/HOL/Library/FuncSet",
   "Eval_Examples",
   "Normalization_by_Evaluation",
   "Hebrew",
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/ex/ReflectionEx.thy
--- a/src/HOL/ex/ReflectionEx.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/ex/ReflectionEx.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -5,7 +5,7 @@
 header {* Examples for generic reflection and reification *}
 
 theory ReflectionEx
-imports Reflection
+imports "~~/src/HOL/Library/Reflection"
 begin
 
 text{* This theory presents two methods: reify and reflection *}
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/ex/Sorting.thy
--- a/src/HOL/ex/Sorting.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/ex/Sorting.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -7,7 +7,7 @@
 header{*Sorting: Basic Theory*}
 
 theory Sorting
-imports Main Multiset
+imports Main "~~/src/HOL/Library/Multiset"
 begin
 
 consts
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/ex/Tarski.thy
--- a/src/HOL/ex/Tarski.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/ex/Tarski.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -1,12 +1,11 @@
 (*  Title:      HOL/ex/Tarski.thy
-    ID:         $Id$
     Author:     Florian Kammüller, Cambridge University Computer Laboratory
 *)
 
 header {* The Full Theorem of Tarski *}
 
 theory Tarski
-imports Main FuncSet
+imports Main "~~/src/HOL/Library/FuncSet"
 begin
 
 text {*
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/ex/Termination.thy
--- a/src/HOL/ex/Termination.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/ex/Termination.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -6,7 +6,7 @@
 header {* Examples and regression tests for automated termination proofs *}
  
 theory Termination
-imports Main Multiset
+imports Main "~~/src/HOL/Library/Multiset"
 begin
 
 subsection {* Manually giving termination relations using @{text relation} and
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/ex/ThreeDivides.thy
--- a/src/HOL/ex/ThreeDivides.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/ex/ThreeDivides.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -5,7 +5,7 @@
 header {* Three Divides Theorem *}
 
 theory ThreeDivides
-imports Main LaTeXsugar
+imports Main "~~/src/HOL/Library/LaTeXsugar"
 begin
 
 subsection {* Abstract *}
diff -r 35f30e07fe0d -r 64cd30d6b0b8 src/HOL/ex/While_Combinator_Example.thy
--- a/src/HOL/ex/While_Combinator_Example.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/src/HOL/ex/While_Combinator_Example.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -6,7 +6,7 @@
 header {* An application of the While combinator *}
 
 theory While_Combinator_Example
-imports While_Combinator
+imports "~~/src/HOL/Library/While_Combinator"
 begin
 
 text {* Computation of the @{term lfp} on finite sets via