# HG changeset patch
# User wenzelm
# Date 1503082067 -7200
# Node ID cc19f7ca2ed6f49c1e8b8e551c0f76e95d7aa7a1
# Parent  450cefec7c118095d10856a262e155723f203c9e
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;

diff -r 450cefec7c11 -r cc19f7ca2ed6 src/Benchmarks/Datatype_Benchmark/IsaFoR.thy
--- a/src/Benchmarks/Datatype_Benchmark/IsaFoR.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/Benchmarks/Datatype_Benchmark/IsaFoR.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -8,7 +8,7 @@
 section \<open>Benchmark Consisting of Datatypes Defined in IsaFoR\<close>
 
 theory IsaFoR
-imports Real
+imports HOL.Real
 begin
 
 datatype (discs_sels) ('f, 'l) lab =
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/Benchmarks/Datatype_Benchmark/Misc_N2M.thy
--- a/src/Benchmarks/Datatype_Benchmark/Misc_N2M.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/Benchmarks/Datatype_Benchmark/Misc_N2M.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -8,7 +8,7 @@
 section \<open>Miscellaneous Tests for the Nested-to-Mutual Reduction\<close>
 
 theory Misc_N2M
-imports "~~/src/HOL/Library/BNF_Axiomatization"
+imports "HOL-Library.BNF_Axiomatization"
 begin
 
 declare [[typedef_overloaded]]
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy
--- a/src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,5 +1,5 @@
 theory Needham_Schroeder_Base
-imports Main "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
+imports Main "HOL-Library.Predicate_Compile_Quickcheck"
 begin
 
 datatype agent = Alice | Bob | Spy
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/CCL/Set.thy
--- a/src/CCL/Set.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/CCL/Set.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,7 +1,7 @@
 section \<open>Extending FOL by a modified version of HOL set theory\<close>
 
 theory Set
-imports "~~/src/FOL/FOL"
+imports FOL
 begin
 
 declare [[eta_contract]]
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/Doc/Codegen/Adaptation.thy
--- a/src/Doc/Codegen/Adaptation.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/Doc/Codegen/Adaptation.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,5 +1,5 @@
 theory Adaptation
-imports Setup
+imports Codegen_Basics.Setup
 begin
 
 setup %invisible \<open>Code_Target.add_derived_target ("\<SML>", [("SML", I)])
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/Doc/Codegen/Computations.thy
--- a/src/Doc/Codegen/Computations.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/Doc/Codegen/Computations.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,7 +1,7 @@
 theory Computations
-  imports Setup
-    "~~/src/HOL/Library/Code_Target_Int"
-    "~~/src/HOL/Library/Code_Char"
+  imports Codegen_Basics.Setup
+    "HOL-Library.Code_Target_Int"
+    "HOL-Library.Code_Char"
 begin
 
 section \<open>Computations \label{sec:computations}\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/Doc/Codegen/Evaluation.thy
--- a/src/Doc/Codegen/Evaluation.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/Doc/Codegen/Evaluation.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,5 +1,5 @@
 theory Evaluation
-imports Setup
+imports Codegen_Basics.Setup
 begin (*<*)
 
 ML \<open>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/Doc/Codegen/Further.thy
--- a/src/Doc/Codegen/Further.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/Doc/Codegen/Further.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,5 +1,5 @@
 theory Further
-imports Setup
+imports Codegen_Basics.Setup
 begin
 
 section \<open>Further issues \label{sec:further}\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/Doc/Codegen/Inductive_Predicate.thy
--- a/src/Doc/Codegen/Inductive_Predicate.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/Doc/Codegen/Inductive_Predicate.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,5 +1,5 @@
 theory Inductive_Predicate
-imports Setup
+imports Codegen_Basics.Setup
 begin
 
 (*<*)
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/Doc/Codegen/Introduction.thy
--- a/src/Doc/Codegen/Introduction.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/Doc/Codegen/Introduction.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,5 +1,5 @@
 theory Introduction
-imports Setup
+imports Codegen_Basics.Setup
 begin (*<*)
 
 ML \<open>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/Doc/Codegen/Refinement.thy
--- a/src/Doc/Codegen/Refinement.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/Doc/Codegen/Refinement.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,5 +1,5 @@
 theory Refinement
-imports Setup
+imports Codegen_Basics.Setup
 begin
 
 section \<open>Program and datatype refinement \label{sec:refinement}\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/Doc/Codegen/Setup.thy
--- a/src/Doc/Codegen/Setup.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/Doc/Codegen/Setup.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,10 +1,10 @@
 theory Setup
 imports
   Complex_Main
-  "~~/src/HOL/Library/Dlist"
-  "~~/src/HOL/Library/RBT"
-  "~~/src/HOL/Library/Mapping"
-  "~~/src/HOL/Library/IArray"
+  "HOL-Library.Dlist"
+  "HOL-Library.RBT"
+  "HOL-Library.Mapping"
+  "HOL-Library.IArray"
 begin
 
 ML_file "../antiquote_setup.ML"
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/Doc/Corec/Corec.thy
--- a/src/Doc/Corec/Corec.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/Doc/Corec/Corec.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -9,8 +9,8 @@
 *)
 
 theory Corec
-imports Main "../Datatypes/Setup" "~~/src/HOL/Library/BNF_Corec"
-  "~~/src/HOL/Library/FSet"
+imports Main Datatypes.Setup "HOL-Library.BNF_Corec"
+  "HOL-Library.FSet"
 begin
 
 section \<open>Introduction
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -12,11 +12,11 @@
 theory Datatypes
 imports
   Setup
-  "~~/src/HOL/Library/BNF_Axiomatization"
-  "~~/src/HOL/Library/Cardinal_Notations"
-  "~~/src/HOL/Library/Countable"
-  "~~/src/HOL/Library/FSet"
-  "~~/src/HOL/Library/Simps_Case_Conv"
+  "HOL-Library.BNF_Axiomatization"
+  "HOL-Library.Cardinal_Notations"
+  "HOL-Library.Countable"
+  "HOL-Library.FSet"
+  "HOL-Library.Simps_Case_Conv"
 begin
 
 section \<open>Introduction
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/Doc/Eisbach/Manual.thy
--- a/src/Doc/Eisbach/Manual.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/Doc/Eisbach/Manual.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,7 +1,7 @@
 (*:maxLineLen=78:*)
 
 theory Manual
-imports Base "~~/src/HOL/Eisbach/Eisbach_Tools"
+imports Base "HOL-Eisbach.Eisbach_Tools"
 begin
 
 chapter \<open>The method command\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/Doc/Eisbach/Preface.thy
--- a/src/Doc/Eisbach/Preface.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/Doc/Eisbach/Preface.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,7 +1,7 @@
 (*:maxLineLen=78:*)
 
 theory Preface
-imports Base "~~/src/HOL/Eisbach/Eisbach_Tools"
+imports Base "HOL-Eisbach.Eisbach_Tools"
 begin
 
 text \<open>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/Doc/Isar_Ref/HOL_Specific.thy
--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -3,11 +3,11 @@
 theory HOL_Specific
   imports
     Main
-    "~~/src/HOL/Library/Old_Datatype"
-    "~~/src/HOL/Library/Old_Recdef"
-    "~~/src/Tools/Adhoc_Overloading"
-    "~~/src/HOL/Library/Dlist"
-    "~~/src/HOL/Library/FSet"
+    "HOL-Library.Old_Datatype"
+    "HOL-Library.Old_Recdef"
+    "HOL-Library.Adhoc_Overloading"
+    "HOL-Library.Dlist"
+    "HOL-Library.FSet"
     Base
 begin
 
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/Doc/Logics_ZF/FOL_examples.thy
--- a/src/Doc/Logics_ZF/FOL_examples.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/Doc/Logics_ZF/FOL_examples.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,6 +1,6 @@
 section{*Examples of Classical Reasoning*}
 
-theory FOL_examples imports "~~/src/FOL/FOL" begin
+theory FOL_examples imports FOL begin
 
 lemma "EX y. ALL x. P(y)-->P(x)"
   --{* @{subgoals[display,indent=0,margin=65]} *}
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/Doc/Logics_ZF/IFOL_examples.thy
--- a/src/Doc/Logics_ZF/IFOL_examples.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/Doc/Logics_ZF/IFOL_examples.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,6 +1,6 @@
 section{*Examples of Intuitionistic Reasoning*}
 
-theory IFOL_examples imports "~~/src/FOL/IFOL" begin
+theory IFOL_examples imports IFOL begin
 
 text{*Quantifier example from the book Logic and Computation*}
 lemma "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/Doc/Logics_ZF/If.thy
--- a/src/Doc/Logics_ZF/If.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/Doc/Logics_ZF/If.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 First-Order Logic: the 'if' example.
 *)
 
-theory If imports "~~/src/FOL/FOL" begin
+theory If imports FOL begin
 
 definition "if" :: "[o,o,o]=>o" where
   "if(P,Q,R) == P&Q | ~P&R"
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/Doc/ROOT
--- a/src/Doc/ROOT	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/Doc/ROOT	Fri Aug 18 20:47:47 2017 +0200
@@ -48,7 +48,7 @@
   options [document_variants = "corec"]
   sessions
     Datatypes
-  theories [document = false] "../Datatypes/Setup"
+  theories [document = false] Datatypes.Setup
   theories Corec
   document_files (in "..")
     "prepare_document"
@@ -249,8 +249,8 @@
   sessions
     "HOL-Library"
   theories [document = false]
-    "~~/src/HOL/Library/LaTeXsugar"
-    "~~/src/HOL/Library/OptionalSugar"
+    "HOL-Library.LaTeXsugar"
+    "HOL-Library.OptionalSugar"
   theories Sugar
   document_files (in "..")
     "prepare_document"
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/Doc/Sugar/Sugar.thy
--- a/src/Doc/Sugar/Sugar.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/Doc/Sugar/Sugar.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,8 +1,8 @@
 (*<*)
 theory Sugar
 imports
-  "~~/src/HOL/Library/LaTeXsugar"
-  "~~/src/HOL/Library/OptionalSugar"
+  "HOL-Library.LaTeXsugar"
+  "HOL-Library.OptionalSugar"
 begin
 no_translations
   ("prop") "P \<and> Q \<Longrightarrow> R" <= ("prop") "P \<Longrightarrow> Q \<Longrightarrow> R"
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/Doc/Typeclass_Hierarchy/Setup.thy
--- a/src/Doc/Typeclass_Hierarchy/Setup.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/Doc/Typeclass_Hierarchy/Setup.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,5 +1,5 @@
 theory Setup
-imports Complex_Main "~~/src/HOL/Library/Multiset" "~~/src/HOL/Library/Lattice_Syntax"
+imports Complex_Main "HOL-Library.Multiset" "HOL-Library.Lattice_Syntax"
 begin
 
 ML_file "../antiquote_setup.ML"
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/Doc/Typeclass_Hierarchy/Typeclass_Hierarchy.thy
--- a/src/Doc/Typeclass_Hierarchy/Typeclass_Hierarchy.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/Doc/Typeclass_Hierarchy/Typeclass_Hierarchy.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,5 +1,5 @@
 theory Typeclass_Hierarchy
-imports Setup
+imports Typeclass_Hierarchy_Basics.Setup
 begin
 
 section \<open>Introduction\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Algebra/Congruence.thy
--- a/src/HOL/Algebra/Congruence.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Algebra/Congruence.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -6,7 +6,7 @@
 theory Congruence
 imports 
   Main
-  "~~/src/HOL/Library/FuncSet"
+  "HOL-Library.FuncSet"
 begin
 
 section \<open>Objects\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Algebra/Divisibility.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -6,7 +6,7 @@
 section \<open>Divisibility in monoids and rings\<close>
 
 theory Divisibility
-  imports "~~/src/HOL/Library/Permutation" Coset Group
+  imports "HOL-Library.Permutation" Coset Group
 begin
 
 section \<open>Factorial Monoids\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Algebra/Exponent.thy
--- a/src/HOL/Algebra/Exponent.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Algebra/Exponent.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -6,7 +6,7 @@
 *)
 
 theory Exponent
-imports Main "~~/src/HOL/Computational_Algebra/Primes"
+imports Main "HOL-Computational_Algebra.Primes"
 begin
 
 section \<open>Sylow's Theorem\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Algebra/Group.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 *)
 
 theory Group
-imports Complete_Lattice "~~/src/HOL/Library/FuncSet"
+imports Complete_Lattice "HOL-Library.FuncSet"
 begin
 
 section \<open>Monoids and Groups\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Algebra/IntRing.thy
--- a/src/HOL/Algebra/IntRing.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Algebra/IntRing.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -4,7 +4,7 @@
 *)
 
 theory IntRing
-imports "~~/src/HOL/Computational_Algebra/Primes" QuotRing Lattice Int
+imports "HOL-Computational_Algebra.Primes" QuotRing Lattice HOL.Int
 begin
 
 section \<open>The Ring of Integers\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Algebra/Order.thy
--- a/src/HOL/Algebra/Order.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Algebra/Order.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -8,7 +8,7 @@
 
 theory Order
 imports 
-  "~~/src/HOL/Library/FuncSet"
+  "HOL-Library.FuncSet"
   Congruence
 begin
 
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Analysis/Arcwise_Connected.thy
--- a/src/HOL/Analysis/Arcwise_Connected.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Analysis/Arcwise_Connected.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Arcwise-connected sets\<close>
 
 theory Arcwise_Connected
-  imports Path_Connected Ordered_Euclidean_Space "~~/src/HOL/Computational_Algebra/Primes"
+  imports Path_Connected Ordered_Euclidean_Space "HOL-Computational_Algebra.Primes"
 
 begin
 
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Complex Analysis Basics\<close>
 
 theory Complex_Analysis_Basics
-imports Equivalence_Lebesgue_Henstock_Integration "~~/src/HOL/Library/Nonpos_Ints"
+imports Equivalence_Lebesgue_Henstock_Integration "HOL-Library.Nonpos_Ints"
 begin
 
 
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -6,7 +6,7 @@
 imports
   Complex_Analysis_Basics
   Summation_Tests
-   "~~/src/HOL/Library/Periodic_Fun"
+   "HOL-Library.Periodic_Fun"
 begin
 
 (* TODO: Figure out what to do with Möbius transformations *)
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Analysis/Continuum_Not_Denumerable.thy
--- a/src/HOL/Analysis/Continuum_Not_Denumerable.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Analysis/Continuum_Not_Denumerable.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -8,7 +8,7 @@
 theory Continuum_Not_Denumerable
 imports
   Complex_Main 
-  "~~/src/HOL/Library/Countable_Set"
+  "HOL-Library.Countable_Set"
 begin
 
 subsection \<open>Abstract\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -11,7 +11,7 @@
 theory Convex_Euclidean_Space
 imports
   Topology_Euclidean_Space
-  "~~/src/HOL/Library/Set_Algebras"
+  "HOL-Library.Set_Algebras"
 begin
 
 lemma swap_continuous: (*move to Topological_Spaces?*)
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Analysis/Determinants.thy
--- a/src/HOL/Analysis/Determinants.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Analysis/Determinants.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -7,7 +7,7 @@
 theory Determinants
 imports
   Cartesian_Euclidean_Space
-  "~~/src/HOL/Library/Permutations"
+  "HOL-Library.Permutations"
 begin
 
 subsection \<open>Trace\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Analysis/Extended_Real_Limits.thy
--- a/src/HOL/Analysis/Extended_Real_Limits.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Analysis/Extended_Real_Limits.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -10,9 +10,9 @@
 theory Extended_Real_Limits
 imports
   Topology_Euclidean_Space
-  "~~/src/HOL/Library/Extended_Real"
-  "~~/src/HOL/Library/Extended_Nonnegative_Real"
-  "~~/src/HOL/Library/Indicator_Function"
+  "HOL-Library.Extended_Real"
+  "HOL-Library.Extended_Nonnegative_Real"
+  "HOL-Library.Indicator_Function"
 begin
 
 lemma compact_UNIV:
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -8,9 +8,9 @@
 imports
   Euclidean_Space
   L2_Norm
-  "~~/src/HOL/Library/Numeral_Type"
-  "~~/src/HOL/Library/Countable_Set"
-  "~~/src/HOL/Library/FuncSet"
+  "HOL-Library.Numeral_Type"
+  "HOL-Library.Countable_Set"
+  "HOL-Library.FuncSet"
 begin
 
 subsection \<open>Finite Cartesian products, with indexing and lambdas.\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Analysis/Gamma_Function.thy
--- a/src/HOL/Analysis/Gamma_Function.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Analysis/Gamma_Function.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -9,8 +9,8 @@
   Conformal_Mappings
   Summation_Tests
   Harmonic_Numbers
-  "~~/src/HOL/Library/Nonpos_Ints"
-  "~~/src/HOL/Library/Periodic_Fun"
+  "HOL-Library.Nonpos_Ints"
+  "HOL-Library.Periodic_Fun"
 begin
 
 text \<open>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Analysis/L2_Norm.thy
--- a/src/HOL/Analysis/L2_Norm.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Analysis/L2_Norm.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Square root of sum of squares\<close>
 
 theory L2_Norm
-imports NthRoot
+imports HOL.NthRoot
 begin
 
 definition
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Analysis/Linear_Algebra.thy
--- a/src/HOL/Analysis/Linear_Algebra.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Analysis/Linear_Algebra.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -7,7 +7,7 @@
 theory Linear_Algebra
 imports
   Euclidean_Space
-  "~~/src/HOL/Library/Infinite_Set"
+  "HOL-Library.Infinite_Set"
 begin
 
 lemma linear_simps:
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Analysis/Measurable.thy
--- a/src/HOL/Analysis/Measurable.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Analysis/Measurable.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -4,7 +4,7 @@
 theory Measurable
   imports
     Sigma_Algebra
-    "~~/src/HOL/Library/Order_Continuity"
+    "HOL-Library.Order_Continuity"
 begin
 
 subsection \<open>Measurability prover\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Analysis/Measure_Space.thy
--- a/src/HOL/Analysis/Measure_Space.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Analysis/Measure_Space.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -8,7 +8,7 @@
 
 theory Measure_Space
 imports
-  Measurable "~~/src/HOL/Library/Extended_Nonnegative_Real"
+  Measurable "HOL-Library.Extended_Nonnegative_Real"
 begin
 
 subsection "Relate extended reals and the indicator function"
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Analysis/Norm_Arith.thy
--- a/src/HOL/Analysis/Norm_Arith.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Analysis/Norm_Arith.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>General linear decision procedure for normed spaces\<close>
 
 theory Norm_Arith
-imports "~~/src/HOL/Library/Sum_of_Squares"
+imports "HOL-Library.Sum_of_Squares"
 begin
 
 (* FIXME: move elsewhere *)
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Analysis/Ordered_Euclidean_Space.thy
--- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,7 +1,7 @@
 theory Ordered_Euclidean_Space
 imports
   Cartesian_Euclidean_Space
-  "~~/src/HOL/Library/Product_Order"
+  "HOL-Library.Product_Order"
 begin
 
 subsection \<open>An ordering on euclidean spaces that will allow us to talk about intervals\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Analysis/Product_Vector.thy
--- a/src/HOL/Analysis/Product_Vector.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Analysis/Product_Vector.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -7,7 +7,7 @@
 theory Product_Vector
 imports
   Inner_Product
-  "~~/src/HOL/Library/Product_Plus"
+  "HOL-Library.Product_Plus"
 begin
 
 subsection \<open>Product is a real vector space\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Analysis/Sigma_Algebra.thy
--- a/src/HOL/Analysis/Sigma_Algebra.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Analysis/Sigma_Algebra.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -10,11 +10,11 @@
 theory Sigma_Algebra
 imports
   Complex_Main
-  "~~/src/HOL/Library/Countable_Set"
-  "~~/src/HOL/Library/FuncSet"
-  "~~/src/HOL/Library/Indicator_Function"
-  "~~/src/HOL/Library/Extended_Nonnegative_Real"
-  "~~/src/HOL/Library/Disjoint_Sets"
+  "HOL-Library.Countable_Set"
+  "HOL-Library.FuncSet"
+  "HOL-Library.Indicator_Function"
+  "HOL-Library.Extended_Nonnegative_Real"
+  "HOL-Library.Disjoint_Sets"
 begin
 
 text \<open>Sigma algebras are an elementary concept in measure
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Analysis/Summation_Tests.thy
--- a/src/HOL/Analysis/Summation_Tests.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Analysis/Summation_Tests.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -7,9 +7,9 @@
 theory Summation_Tests
 imports
   Complex_Main
-  "~~/src/HOL/Library/Discrete"
-  "~~/src/HOL/Library/Extended_Real"
-  "~~/src/HOL/Library/Liminf_Limsup"
+  "HOL-Library.Discrete"
+  "HOL-Library.Extended_Real"
+  "HOL-Library.Liminf_Limsup"
 begin
 
 text \<open>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -8,9 +8,9 @@
 
 theory Topology_Euclidean_Space
 imports
-  "~~/src/HOL/Library/Indicator_Function"
-  "~~/src/HOL/Library/Countable_Set"
-  "~~/src/HOL/Library/FuncSet"
+  "HOL-Library.Indicator_Function"
+  "HOL-Library.Countable_Set"
+  "HOL-Library.FuncSet"
   Linear_Algebra
   Norm_Arith
 begin
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Analysis/ex/Approximations.thy
--- a/src/HOL/Analysis/ex/Approximations.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Analysis/ex/Approximations.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,7 +1,7 @@
 section \<open>Numeric approximations to Constants\<close>
 
 theory Approximations
-imports "../Complex_Transcendental" "../Harmonic_Numbers"
+imports "HOL-Analysis.Complex_Transcendental" "HOL-Analysis.Harmonic_Numbers"
 begin
 
 text \<open>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Analysis/ex/Circle_Area.thy
--- a/src/HOL/Analysis/ex/Circle_Area.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Analysis/ex/Circle_Area.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -7,7 +7,7 @@
 section \<open>The area of a circle\<close>
 
 theory Circle_Area
-imports Complex_Main Interval_Integral
+imports Complex_Main "HOL-Analysis.Interval_Integral"
 begin
 
 lemma plus_emeasure':
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Auth/Smartcard/EventSC.thy
--- a/src/HOL/Auth/Smartcard/EventSC.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Auth/Smartcard/EventSC.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -3,7 +3,7 @@
 theory EventSC
 imports
   "../Message"
-  "~~/src/HOL/Library/Simps_Case_Conv"
+  "HOL-Library.Simps_Case_Conv"
 begin
 
 consts  (*Initial states of agents -- parameter of the construction*)
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Auth/TLS.thy
--- a/src/HOL/Auth/TLS.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Auth/TLS.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -40,7 +40,7 @@
 
 section\<open>The TLS Protocol: Transport Layer Security\<close>
 
-theory TLS imports Public "~~/src/HOL/Library/Nat_Bijection" begin
+theory TLS imports Public "HOL-Library.Nat_Bijection" begin
 
 definition certificate :: "[agent,key] => msg" where
     "certificate A KA == Crypt (priSK Server) \<lbrace>Agent A, Key KA\<rbrace>"
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Bali/Basis.thy
--- a/src/HOL/Bali/Basis.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Bali/Basis.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -4,7 +4,7 @@
 subsection \<open>Definitions extending HOL as logical basis of Bali\<close>
 
 theory Basis
-imports Main "~~/src/HOL/Library/Old_Recdef"
+imports Main "HOL-Library.Old_Recdef"
 begin
 
 subsubsection "misc"
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Cardinals/Cardinal_Arithmetic.thy
--- a/src/HOL/Cardinals/Cardinal_Arithmetic.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -8,7 +8,7 @@
 section \<open>Cardinal Arithmetic\<close>
 
 theory Cardinal_Arithmetic
-imports BNF_Cardinal_Arithmetic Cardinal_Order_Relation
+imports HOL.BNF_Cardinal_Arithmetic Cardinal_Order_Relation
 begin
 
 subsection \<open>Binary sum\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Cardinals/Cardinal_Order_Relation.thy
--- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -8,7 +8,7 @@
 section \<open>Cardinal-Order Relations\<close>
 
 theory Cardinal_Order_Relation
-imports BNF_Cardinal_Order_Relation Wellorder_Constructions
+imports HOL.BNF_Cardinal_Order_Relation Wellorder_Constructions
 begin
 
 declare
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Cardinals/Order_Union.thy
--- a/src/HOL/Cardinals/Order_Union.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Cardinals/Order_Union.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -7,7 +7,7 @@
 section \<open>Order Union\<close>
 
 theory Order_Union
-imports Order_Relation
+imports HOL.Order_Relation
 begin
 
 definition Osum :: "'a rel \<Rightarrow> 'a rel \<Rightarrow> 'a rel"  (infix "Osum" 60) where
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Cardinals/Wellfounded_More.thy
--- a/src/HOL/Cardinals/Wellfounded_More.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Cardinals/Wellfounded_More.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -8,7 +8,7 @@
 section \<open>More on Well-Founded Relations\<close>
 
 theory Wellfounded_More
-imports Wellfounded Order_Relation_More
+imports HOL.Wellfounded Order_Relation_More
 begin
 
 subsection \<open>Well-founded recursion via genuine fixpoints\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Cardinals/Wellorder_Constructions.thy
--- a/src/HOL/Cardinals/Wellorder_Constructions.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Cardinals/Wellorder_Constructions.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -9,8 +9,8 @@
 
 theory Wellorder_Constructions
 imports
-  BNF_Wellorder_Constructions Wellorder_Embedding Order_Union
-  "../Library/Cardinal_Notations"
+  HOL.BNF_Wellorder_Constructions Wellorder_Embedding Order_Union
+  "HOL-Library.Cardinal_Notations"
 begin
 
 declare
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Cardinals/Wellorder_Embedding.thy
--- a/src/HOL/Cardinals/Wellorder_Embedding.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Cardinals/Wellorder_Embedding.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -8,7 +8,7 @@
 section \<open>Well-Order Embeddings\<close>
 
 theory Wellorder_Embedding
-imports BNF_Wellorder_Embedding Fun_More Wellorder_Relation
+imports HOL.BNF_Wellorder_Embedding Fun_More Wellorder_Relation
 begin
 
 subsection \<open>Auxiliaries\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Cardinals/Wellorder_Relation.thy
--- a/src/HOL/Cardinals/Wellorder_Relation.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Cardinals/Wellorder_Relation.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -8,7 +8,7 @@
 section \<open>Well-Order Relations\<close>
 
 theory Wellorder_Relation
-imports BNF_Wellorder_Relation Wellfounded_More
+imports HOL.BNF_Wellorder_Relation Wellfounded_More
 begin
 
 context wo_rel
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Codegenerator_Test/Candidates.thy
--- a/src/HOL/Codegenerator_Test/Candidates.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Codegenerator_Test/Candidates.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -6,15 +6,15 @@
 theory Candidates
 imports
   Complex_Main
-  "~~/src/HOL/Library/Library"
-  "~~/src/HOL/Library/Subseq_Order"
-  "~~/src/HOL/Library/RBT"
-  "~~/src/HOL/Data_Structures/Tree_Map"
-  "~~/src/HOL/Data_Structures/Tree_Set"
-  "~~/src/HOL/Computational_Algebra/Computational_Algebra"
-  "~~/src/HOL/Computational_Algebra/Polynomial_Factorial"
-  "~~/src/HOL/Number_Theory/Eratosthenes"
-  "~~/src/HOL/ex/Records"
+  "HOL-Library.Library"
+  "HOL-Library.Subseq_Order"
+  "HOL-Library.RBT"
+  "HOL-Data_Structures.Tree_Map"
+  "HOL-Data_Structures.Tree_Set"
+  "HOL-Computational_Algebra.Computational_Algebra"
+  "HOL-Computational_Algebra.Polynomial_Factorial"
+  "HOL-Number_Theory.Eratosthenes"
+  "HOL-ex.Records"
 begin
 
 text \<open>Drop technical stuff from @{theory Quickcheck_Narrowing} which is tailored towards Haskell\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Codegenerator_Test/Code_Test_GHC.thy
--- a/src/HOL/Codegenerator_Test/Code_Test_GHC.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Codegenerator_Test/Code_Test_GHC.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -4,7 +4,7 @@
 Test case for test_code on GHC
 *)
 
-theory Code_Test_GHC imports "../Library/Code_Test" begin
+theory Code_Test_GHC imports "HOL-Library.Code_Test" begin
 
 test_code "(14 + 7 * -12 :: integer) = 140 div -2" in GHC
 
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Codegenerator_Test/Code_Test_MLton.thy
--- a/src/HOL/Codegenerator_Test/Code_Test_MLton.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Codegenerator_Test/Code_Test_MLton.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -4,7 +4,7 @@
 Test case for test_code on MLton
 *)
 
-theory Code_Test_MLton imports  "../Library/Code_Test" begin
+theory Code_Test_MLton imports  "HOL-Library.Code_Test" begin
 
 test_code "14 + 7 * -12 = (140 div -2 :: integer)" in MLton
 
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Codegenerator_Test/Code_Test_OCaml.thy
--- a/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -4,7 +4,7 @@
 Test case for test_code on OCaml
 *)
 
-theory Code_Test_OCaml imports  "../Library/Code_Test" begin
+theory Code_Test_OCaml imports  "HOL-Library.Code_Test" begin
 
 test_code "14 + 7 * -12 = (140 div -2 :: integer)" in OCaml
 
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Codegenerator_Test/Code_Test_PolyML.thy
--- a/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -4,7 +4,7 @@
 Test case for test_code on PolyML
 *)
 
-theory Code_Test_PolyML imports  "../Library/Code_Test" begin
+theory Code_Test_PolyML imports  "HOL-Library.Code_Test" begin
 
 test_code "14 + 7 * -12 = (140 div -2 :: integer)" in PolyML
 
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Codegenerator_Test/Code_Test_SMLNJ.thy
--- a/src/HOL/Codegenerator_Test/Code_Test_SMLNJ.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Codegenerator_Test/Code_Test_SMLNJ.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -4,7 +4,7 @@
 Test case for test_code on SMLNJ
 *)
 
-theory Code_Test_SMLNJ imports  "../Library/Code_Test" begin
+theory Code_Test_SMLNJ imports  "HOL-Library.Code_Test" begin
 
 test_code "14 + 7 * -12 = (140 div -2 :: integer)" in SMLNJ
 
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Codegenerator_Test/Code_Test_Scala.thy
--- a/src/HOL/Codegenerator_Test/Code_Test_Scala.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Codegenerator_Test/Code_Test_Scala.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -4,7 +4,7 @@
 Test case for test_code on Scala
 *)
 
-theory Code_Test_Scala imports  "../Library/Code_Test" begin
+theory Code_Test_Scala imports  "HOL-Library.Code_Test" begin
 
 declare [[scala_case_insensitive]]
 
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Codegenerator_Test/Generate.thy
--- a/src/HOL/Codegenerator_Test/Generate.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Codegenerator_Test/Generate.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -6,8 +6,8 @@
 theory Generate
 imports
   Candidates
-  "~~/src/HOL/Library/AList_Mapping"
-  "~~/src/HOL/Library/Finite_Lattice"
+  "HOL-Library.AList_Mapping"
+  "HOL-Library.Finite_Lattice"
 begin
 
 text \<open>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Codegenerator_Test/Generate_Binary_Nat.thy
--- a/src/HOL/Codegenerator_Test/Generate_Binary_Nat.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Codegenerator_Test/Generate_Binary_Nat.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -6,9 +6,9 @@
 theory Generate_Binary_Nat
 imports
   Candidates
-  "~~/src/HOL/Library/AList_Mapping"
-  "~~/src/HOL/Library/Finite_Lattice"
-  "~~/src/HOL/Library/Code_Binary_Nat"
+  "HOL-Library.AList_Mapping"
+  "HOL-Library.Finite_Lattice"
+  "HOL-Library.Code_Binary_Nat"
 begin
 
 text \<open>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy
--- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -6,9 +6,9 @@
 theory Generate_Efficient_Datastructures
 imports
   Candidates
-  "~~/src/HOL/Library/DAList_Multiset"
-  "~~/src/HOL/Library/RBT_Mapping"
-  "~~/src/HOL/Library/RBT_Set"
+  "HOL-Library.DAList_Multiset"
+  "HOL-Library.RBT_Mapping"
+  "HOL-Library.RBT_Set"
 begin
 
 text \<open>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Codegenerator_Test/Generate_Pretty_Char.thy
--- a/src/HOL/Codegenerator_Test/Generate_Pretty_Char.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Codegenerator_Test/Generate_Pretty_Char.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -6,9 +6,9 @@
 theory Generate_Pretty_Char
 imports
   Candidates
-  "~~/src/HOL/Library/AList_Mapping"
-  "~~/src/HOL/Library/Finite_Lattice"
-  "~~/src/HOL/Library/Code_Char"
+  "HOL-Library.AList_Mapping"
+  "HOL-Library.Finite_Lattice"
+  "HOL-Library.Code_Char"
 begin
 
 text \<open>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Codegenerator_Test/Generate_Target_Nat.thy
--- a/src/HOL/Codegenerator_Test/Generate_Target_Nat.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Codegenerator_Test/Generate_Target_Nat.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -6,9 +6,9 @@
 theory Generate_Target_Nat
 imports
   Candidates
-  "~~/src/HOL/Library/AList_Mapping"
-  "~~/src/HOL/Library/Finite_Lattice"
-  "~~/src/HOL/Library/Code_Target_Numeral"
+  "HOL-Library.AList_Mapping"
+  "HOL-Library.Finite_Lattice"
+  "HOL-Library.Code_Target_Numeral"
 begin
 
 text \<open>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Computational_Algebra/Factorial_Ring.thy
--- a/src/HOL/Computational_Algebra/Factorial_Ring.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Computational_Algebra/Factorial_Ring.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -8,7 +8,7 @@
 theory Factorial_Ring
 imports
   Main
-  "~~/src/HOL/Library/Multiset"
+  "HOL-Library.Multiset"
 begin
 
 subsection \<open>Irreducible and prime elements\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Computational_Algebra/Polynomial.thy
--- a/src/HOL/Computational_Algebra/Polynomial.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -9,9 +9,9 @@
 
 theory Polynomial
 imports
-  "~~/src/HOL/Deriv"
-  "~~/src/HOL/Library/More_List"
-  "~~/src/HOL/Library/Infinite_Set"
+  HOL.Deriv
+  "HOL-Library.More_List"
+  "HOL-Library.Infinite_Set"
 begin
 
 subsection \<open>Auxiliary: operations for lists (later) representing coefficients\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Computational_Algebra/Primes.thy
--- a/src/HOL/Computational_Algebra/Primes.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Computational_Algebra/Primes.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -39,7 +39,7 @@
 section \<open>Primes\<close>
 
 theory Primes
-imports "~~/src/HOL/Binomial" Euclidean_Algorithm
+imports HOL.Binomial Euclidean_Algorithm
 begin
 
 (* As a simp or intro rule,
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Corec_Examples/LFilter.thy
--- a/src/HOL/Corec_Examples/LFilter.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Corec_Examples/LFilter.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -10,7 +10,7 @@
 section \<open>The Filter Function on Lazy Lists\<close>
 
 theory LFilter
-imports "~~/src/HOL/Library/BNF_Corec"
+imports "HOL-Library.BNF_Corec"
 begin
 
 codatatype (lset: 'a) llist =
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Corec_Examples/Paper_Examples.thy
--- a/src/HOL/Corec_Examples/Paper_Examples.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Corec_Examples/Paper_Examples.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -9,7 +9,7 @@
 section \<open>Small Examples from the Paper ``Friends with Benefits''\<close>
 
 theory Paper_Examples
-imports "~~/src/HOL/Library/BNF_Corec" "~~/src/HOL/Library/FSet" Complex_Main
+imports "HOL-Library.BNF_Corec" "HOL-Library.FSet" Complex_Main
 begin
 
 section \<open>Examples from the introduction\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Corec_Examples/Stream_Processor.thy
--- a/src/HOL/Corec_Examples/Stream_Processor.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Corec_Examples/Stream_Processor.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -10,7 +10,7 @@
 section \<open>Stream Processors---A Syntactic Representation of Continuous Functions on Streams\<close>
 
 theory Stream_Processor
-imports "~~/src/HOL/Library/BNF_Corec" "~~/src/HOL/Library/Stream"
+imports "HOL-Library.BNF_Corec" "HOL-Library.Stream"
 begin
 
 datatype (discs_sels) ('a, 'b, 'c) sp\<^sub>\<mu> =
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Corec_Examples/Tests/GPV_Bare_Bones.thy
--- a/src/HOL/Corec_Examples/Tests/GPV_Bare_Bones.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Corec_Examples/Tests/GPV_Bare_Bones.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -9,7 +9,7 @@
 section \<open>A Bare Bones Version of Generative Probabilistic Values (GPVs)\<close>
 
 theory GPV_Bare_Bones
-imports "~~/src/HOL/Library/BNF_Corec"
+imports "HOL-Library.BNF_Corec"
 begin
 
 datatype 'a pmf = return_pmf 'a
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Corec_Examples/Tests/Iterate_GPV.thy
--- a/src/HOL/Corec_Examples/Tests/Iterate_GPV.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Corec_Examples/Tests/Iterate_GPV.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,6 +1,6 @@
 theory Iterate_GPV imports
-  "~~/src/HOL/Library/BNF_Axiomatization"
-  "~~/src/HOL/Library/BNF_Corec"
+  "HOL-Library.BNF_Axiomatization"
+  "HOL-Library.BNF_Corec"
 begin
 
 declare [[typedef_overloaded]]
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Corec_Examples/Tests/Merge_A.thy
--- a/src/HOL/Corec_Examples/Tests/Merge_A.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Corec_Examples/Tests/Merge_A.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -9,7 +9,7 @@
 section \<open>Tests Theory Merges\<close>
 
 theory Merge_A
-imports "~~/src/HOL/Library/BNF_Corec"
+imports "HOL-Library.BNF_Corec"
 begin
 
 codatatype 'a ta = Ca (sa1: 'a) (sa2: "'a ta")
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Corec_Examples/Tests/Merge_Poly.thy
--- a/src/HOL/Corec_Examples/Tests/Merge_Poly.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Corec_Examples/Tests/Merge_Poly.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -9,7 +9,7 @@
 section \<open>Tests Polymorphic Merges\<close>
 
 theory Merge_Poly
-imports "~~/src/HOL/Library/BNF_Corec"
+imports "HOL-Library.BNF_Corec"
 begin
 
 subsection \<open>A Monomorphic Example\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Corec_Examples/Tests/Misc_Mono.thy
--- a/src/HOL/Corec_Examples/Tests/Misc_Mono.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Corec_Examples/Tests/Misc_Mono.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -9,7 +9,7 @@
 section \<open>Miscellaneous Monomorphic Examples\<close>
 
 theory Misc_Mono
-imports "~~/src/HOL/Library/BNF_Corec"
+imports "HOL-Library.BNF_Corec"
 begin
 
 codatatype T0 =
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Corec_Examples/Tests/Misc_Poly.thy
--- a/src/HOL/Corec_Examples/Tests/Misc_Poly.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Corec_Examples/Tests/Misc_Poly.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -9,7 +9,7 @@
 section \<open>Miscellaneous Polymorphic Examples\<close>
 
 theory Misc_Poly
-imports "~~/src/HOL/Library/BNF_Corec"
+imports "HOL-Library.BNF_Corec"
 begin
 
 codatatype ('a, 'b) T0 =
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Corec_Examples/Tests/Simple_Nesting.thy
--- a/src/HOL/Corec_Examples/Tests/Simple_Nesting.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Corec_Examples/Tests/Simple_Nesting.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -9,7 +9,7 @@
 section \<open>Tests "corec"'s Parsing of Map Functions\<close>
 
 theory Simple_Nesting
-imports "~~/src/HOL/Library/BNF_Corec"
+imports "HOL-Library.BNF_Corec"
 begin
 
 subsection \<open>Corecursion via Map Functions\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Corec_Examples/Tests/Small_Concrete.thy
--- a/src/HOL/Corec_Examples/Tests/Small_Concrete.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Corec_Examples/Tests/Small_Concrete.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -9,7 +9,7 @@
 section \<open>Small Concrete Examples\<close>
 
 theory Small_Concrete
-imports "~~/src/HOL/Library/BNF_Corec"
+imports "HOL-Library.BNF_Corec"
 begin
 
 subsection \<open>Streams of Natural Numbers\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Corec_Examples/Tests/Stream_Friends.thy
--- a/src/HOL/Corec_Examples/Tests/Stream_Friends.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Corec_Examples/Tests/Stream_Friends.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -9,7 +9,7 @@
 section \<open>Friendly Functions on Streams\<close>
 
 theory Stream_Friends
-imports "~~/src/HOL/Library/BNF_Corec"
+imports "HOL-Library.BNF_Corec"
 begin
 
 codatatype 'a stream = SCons (shd: 'a) (stl: "'a stream")
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Corec_Examples/Tests/TLList_Friends.thy
--- a/src/HOL/Corec_Examples/Tests/TLList_Friends.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Corec_Examples/Tests/TLList_Friends.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -9,7 +9,7 @@
 section \<open>Friendly Functions on Terminated Lists\<close>
 
 theory TLList_Friends
-imports "~~/src/HOL/Library/BNF_Corec"
+imports "HOL-Library.BNF_Corec"
 begin
 
 codatatype ('a, 'b) tllist =
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Corec_Examples/Tests/Type_Class.thy
--- a/src/HOL/Corec_Examples/Tests/Type_Class.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Corec_Examples/Tests/Type_Class.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -9,7 +9,7 @@
 section \<open>Tests Type Class Instances as Friends\<close>
 
 theory Type_Class
-imports "~~/src/HOL/Library/BNF_Corec" "~~/src/HOL/Library/Stream"
+imports "HOL-Library.BNF_Corec" "HOL-Library.Stream"
 begin
 
 instantiation stream :: (plus) plus
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Data_Structures/AVL_Set.thy
--- a/src/HOL/Data_Structures/AVL_Set.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Data_Structures/AVL_Set.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -9,7 +9,7 @@
 imports
  Cmp
  Isin2
-  "~~/src/HOL/Number_Theory/Fib"
+  "HOL-Number_Theory.Fib"
 begin
 
 type_synonym 'a avl_tree = "('a,nat) tree"
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Data_Structures/Balance.thy
--- a/src/HOL/Data_Structures/Balance.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Data_Structures/Balance.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 theory Balance
 imports
   Complex_Main
-  "~~/src/HOL/Library/Tree"
+  "HOL-Library.Tree"
 begin
 
 (* The following two lemmas should go into theory \<open>Tree\<close>, except that that
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Data_Structures/Brother12_Set.thy
--- a/src/HOL/Data_Structures/Brother12_Set.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Data_Structures/Brother12_Set.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -6,7 +6,7 @@
 imports
   Cmp
   Set_by_Ordered
-  "~~/src/HOL/Number_Theory/Fib"
+  "HOL-Number_Theory.Fib"
 begin
 
 subsection \<open>Data Type and Operations\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Data_Structures/Priority_Queue.thy
--- a/src/HOL/Data_Structures/Priority_Queue.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Data_Structures/Priority_Queue.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -3,7 +3,7 @@
 section \<open>Priority Queue Interface\<close>
 
 theory Priority_Queue
-imports "~~/src/HOL/Library/Multiset"
+imports "HOL-Library.Multiset"
 begin
 
 text \<open>Priority queue interface:\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Data_Structures/Splay_Set.thy
--- a/src/HOL/Data_Structures/Splay_Set.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Data_Structures/Splay_Set.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -7,7 +7,7 @@
 
 theory Splay_Set
 imports
-  "~~/src/HOL/Library/Tree"
+  "HOL-Library.Tree"
   Set_by_Ordered
   Cmp
 begin
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Data_Structures/Tree_Set.thy
--- a/src/HOL/Data_Structures/Tree_Set.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Data_Structures/Tree_Set.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -4,7 +4,7 @@
 
 theory Tree_Set
 imports
-  "~~/src/HOL/Library/Tree"
+  "HOL-Library.Tree"
   Cmp
   Set_by_Ordered
 begin
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Datatype_Examples/Compat.thy
--- a/src/HOL/Datatype_Examples/Compat.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Datatype_Examples/Compat.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -8,7 +8,7 @@
 section \<open>Tests for Compatibility with the Old Datatype Package\<close>
 
 theory Compat
-imports "~~/src/HOL/Library/Old_Datatype"
+imports "HOL-Library.Old_Datatype"
 begin
 
 subsection \<open>Viewing and Registering New-Style Datatypes as Old-Style Ones\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Datatype_Examples/Derivation_Trees/Gram_Lang.thy
--- a/src/HOL/Datatype_Examples/Derivation_Trees/Gram_Lang.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Datatype_Examples/Derivation_Trees/Gram_Lang.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -8,7 +8,7 @@
 section \<open>Language of a Grammar\<close>
 
 theory Gram_Lang
-imports DTree "~~/src/HOL/Library/Infinite_Set"
+imports DTree "HOL-Library.Infinite_Set"
 begin
 
 
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Datatype_Examples/Derivation_Trees/Prelim.thy
--- a/src/HOL/Datatype_Examples/Derivation_Trees/Prelim.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Datatype_Examples/Derivation_Trees/Prelim.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -8,7 +8,7 @@
 section \<open>Preliminaries\<close>
 
 theory Prelim
-imports "~~/src/HOL/Library/FSet"
+imports "HOL-Library.FSet"
 begin
 
 notation BNF_Def.convol ("\<langle>(_,/ _)\<rangle>")
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Datatype_Examples/Koenig.thy
--- a/src/HOL/Datatype_Examples/Koenig.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Datatype_Examples/Koenig.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -9,7 +9,7 @@
 section \<open>Koenig's Lemma\<close>
 
 theory Koenig
-imports TreeFI "~~/src/HOL/Library/Stream"
+imports TreeFI "HOL-Library.Stream"
 begin
 
 (* infinite trees: *)
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Datatype_Examples/Lambda_Term.thy
--- a/src/HOL/Datatype_Examples/Lambda_Term.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Datatype_Examples/Lambda_Term.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -9,7 +9,7 @@
 section \<open>Lambda-Terms\<close>
 
 theory Lambda_Term
-imports "~~/src/HOL/Library/FSet"
+imports "HOL-Library.FSet"
 begin
 
 section \<open>Datatype definition\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Datatype_Examples/Misc_Codatatype.thy
--- a/src/HOL/Datatype_Examples/Misc_Codatatype.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Datatype_Examples/Misc_Codatatype.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -10,7 +10,7 @@
 section \<open>Miscellaneous Codatatype Definitions\<close>
 
 theory Misc_Codatatype
-imports "~~/src/HOL/Library/FSet"
+imports "HOL-Library.FSet"
 begin
 
 codatatype simple = X1 | X2 | X3 | X4
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Datatype_Examples/Misc_Datatype.thy
--- a/src/HOL/Datatype_Examples/Misc_Datatype.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Datatype_Examples/Misc_Datatype.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -10,7 +10,7 @@
 section \<open>Miscellaneous Datatype Definitions\<close>
 
 theory Misc_Datatype
-imports "~~/src/HOL/Library/Countable" "~~/src/HOL/Library/FSet"
+imports "HOL-Library.Countable" "HOL-Library.FSet"
 begin
 
 datatype (discs_sels) simple = X1 | X2 | X3 | X4
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Datatype_Examples/Process.thy
--- a/src/HOL/Datatype_Examples/Process.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Datatype_Examples/Process.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -8,7 +8,7 @@
 section \<open>Processes\<close>
 
 theory Process
-imports "~~/src/HOL/Library/Stream"
+imports "HOL-Library.Stream"
 begin
 
 codatatype 'a process =
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Datatype_Examples/Stream_Processor.thy
--- a/src/HOL/Datatype_Examples/Stream_Processor.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Datatype_Examples/Stream_Processor.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -9,7 +9,7 @@
 section \<open>Stream Processors---A Syntactic Representation of Continuous Functions on Streams\<close>
 
 theory Stream_Processor
-imports "~~/src/HOL/Library/Stream" "~~/src/HOL/Library/BNF_Axiomatization"
+imports "HOL-Library.Stream" "HOL-Library.BNF_Axiomatization"
 begin
 
 declare [[typedef_overloaded]]
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Datatype_Examples/TreeFsetI.thy
--- a/src/HOL/Datatype_Examples/TreeFsetI.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Datatype_Examples/TreeFsetI.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -9,7 +9,7 @@
 section \<open>Finitely Branching Possibly Infinite Trees, with Sets of Children\<close>
 
 theory TreeFsetI
-imports "~~/src/HOL/Library/FSet"
+imports "HOL-Library.FSet"
 begin
 
 codatatype 'a treeFsetI = Tree (lab: 'a) (sub: "'a treeFsetI fset")
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Decision_Procs/Algebra_Aux.thy
--- a/src/HOL/Decision_Procs/Algebra_Aux.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Decision_Procs/Algebra_Aux.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Things that can be added to the Algebra library\<close>
 
 theory Algebra_Aux
-imports "~~/src/HOL/Algebra/Ring"
+imports "HOL-Algebra.Ring"
 begin
 
 definition of_natural :: "('a, 'm) ring_scheme \<Rightarrow> nat \<Rightarrow> 'a" ("\<guillemotleft>_\<guillemotright>\<^sub>\<nat>\<index>") where
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -4,7 +4,7 @@
 theory Approximation
 imports
   Complex_Main
-  "~~/src/HOL/Library/Code_Target_Numeral"
+  "HOL-Library.Code_Target_Numeral"
   Approximation_Bounds
 keywords "approximate" :: diag
 begin
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Decision_Procs/Approximation_Bounds.thy
--- a/src/HOL/Decision_Procs/Approximation_Bounds.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Decision_Procs/Approximation_Bounds.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -11,7 +11,7 @@
 theory Approximation_Bounds
 imports
   Complex_Main
-  "~~/src/HOL/Library/Float"
+  "HOL-Library.Float"
   Dense_Linear_Order
 begin
 
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Decision_Procs/Commutative_Ring.thy
--- a/src/HOL/Decision_Procs/Commutative_Ring.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Decision_Procs/Commutative_Ring.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -10,7 +10,7 @@
 imports
   Conversions
   Algebra_Aux
-  "~~/src/HOL/Library/Code_Target_Numeral"
+  "HOL-Library.Code_Target_Numeral"
 begin
 
 text \<open>Syntax of multivariate polynomials (pol) and polynomial expressions.\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Decision_Procs/Cooper.thy
--- a/src/HOL/Decision_Procs/Cooper.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,8 +5,8 @@
 theory Cooper
 imports
   Complex_Main
-  "~~/src/HOL/Library/Code_Target_Numeral"
-  "~~/src/HOL/Library/Old_Recdef"
+  "HOL-Library.Code_Target_Numeral"
+  "HOL-Library.Old_Recdef"
 begin
 
 (* Periodicity of dvd *)
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Decision_Procs/Ferrack.thy
--- a/src/HOL/Decision_Procs/Ferrack.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -4,7 +4,7 @@
 
 theory Ferrack
 imports Complex_Main Dense_Linear_Order DP_Library
-  "~~/src/HOL/Library/Code_Target_Numeral" "~~/src/HOL/Library/Old_Recdef"
+  "HOL-Library.Code_Target_Numeral" "HOL-Library.Old_Recdef"
 begin
 
 section \<open>Quantifier elimination for \<open>\<real> (0, 1, +, <)\<close>\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -4,7 +4,7 @@
 
 theory MIR
 imports Complex_Main Dense_Linear_Order DP_Library
-  "~~/src/HOL/Library/Code_Target_Numeral" "~~/src/HOL/Library/Old_Recdef"
+  "HOL-Library.Code_Target_Numeral" "HOL-Library.Old_Recdef"
 begin
 
 section \<open>Quantifier elimination for \<open>\<real> (0, 1, +, floor, <)\<close>\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -9,8 +9,8 @@
   Reflected_Multivariate_Polynomial
   Dense_Linear_Order
   DP_Library
-  "~~/src/HOL/Library/Code_Target_Numeral"
-  "~~/src/HOL/Library/Old_Recdef"
+  "HOL-Library.Code_Target_Numeral"
+  "HOL-Library.Old_Recdef"
 begin
 
 subsection \<open>Terms\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Eisbach/Examples_FOL.thy
--- a/src/HOL/Eisbach/Examples_FOL.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Eisbach/Examples_FOL.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Basic Eisbach examples (in FOL)\<close>
 
 theory Examples_FOL
-imports "~~/src/FOL/FOL" Eisbach_Old_Appl_Syntax
+imports FOL Eisbach_Old_Appl_Syntax
 begin
 
 
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/HOLCF/Bifinite.thy
--- a/src/HOL/HOLCF/Bifinite.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/HOLCF/Bifinite.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Profinite and bifinite cpos\<close>
 
 theory Bifinite
-imports Map_Functions Cprod Sprod Sfun Up "~~/src/HOL/Library/Countable"
+imports Map_Functions Cprod Sprod Sfun Up "HOL-Library.Countable"
 begin
 
 default_sort cpo
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/HOLCF/FOCUS/Fstream.thy
--- a/src/HOL/HOLCF/FOCUS/Fstream.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/HOLCF/FOCUS/Fstream.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -9,7 +9,7 @@
 section \<open>FOCUS flat streams\<close>
 
 theory Fstream
-imports "~~/src/HOL/HOLCF/Library/Stream"
+imports "HOLCF-Library.Stream"
 begin
 
 default_sort type
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/HOLCF/FOCUS/Fstreams.thy
--- a/src/HOL/HOLCF/FOCUS/Fstreams.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/HOLCF/FOCUS/Fstreams.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -7,7 +7,7 @@
 *)
 
 theory Fstreams
-imports "~~/src/HOL/HOLCF/Library/Stream"
+imports "HOLCF-Library.Stream"
 begin
 
 default_sort type
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/HOLCF/FOCUS/Stream_adm.thy
--- a/src/HOL/HOLCF/FOCUS/Stream_adm.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/HOLCF/FOCUS/Stream_adm.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Admissibility for streams\<close>
 
 theory Stream_adm
-imports "~~/src/HOL/HOLCF/Library/Stream" "~~/src/HOL/Library/Order_Continuity"
+imports "HOLCF-Library.Stream" "HOL-Library.Order_Continuity"
 begin
 
 definition
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/HOLCF/IMP/Denotational.thy
--- a/src/HOL/HOLCF/IMP/Denotational.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/HOLCF/IMP/Denotational.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 
 section "Denotational Semantics of Commands in HOLCF"
 
-theory Denotational imports HOLCF "~~/src/HOL/IMP/Big_Step" begin
+theory Denotational imports HOLCF "HOL-IMP.Big_Step" begin
 
 subsection "Definition"
 
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/HOLCF/IOA/ABP/Abschannel.thy
--- a/src/HOL/HOLCF/IOA/ABP/Abschannel.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/HOLCF/IOA/ABP/Abschannel.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>The transmission channel\<close>
 
 theory Abschannel
-imports "../IOA" Action Lemmas
+imports IOA.IOA Action Lemmas
 begin
 
 datatype 'a abs_action = S 'a | R 'a
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/HOLCF/IOA/ABP/Abschannel_finite.thy
--- a/src/HOL/HOLCF/IOA/ABP/Abschannel_finite.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/HOLCF/IOA/ABP/Abschannel_finite.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>The transmission channel -- finite version\<close>
 
 theory Abschannel_finite
-imports Abschannel "../IOA" Action Lemmas
+imports Abschannel IOA.IOA Action Lemmas
 begin
 
 primrec reverse :: "'a list => 'a list"
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/HOLCF/IOA/ABP/Correctness.thy
--- a/src/HOL/HOLCF/IOA/ABP/Correctness.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/HOLCF/IOA/ABP/Correctness.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>The main correctness proof: System_fin implements System\<close>
 
 theory Correctness
-imports "../IOA" Env Impl Impl_finite
+imports IOA.IOA Env Impl Impl_finite
 begin
 
 ML_file "Check.ML"
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/HOLCF/IOA/ABP/Env.thy
--- a/src/HOL/HOLCF/IOA/ABP/Env.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/HOLCF/IOA/ABP/Env.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>The environment\<close>
 
 theory Env
-imports "../IOA" Action
+imports IOA.IOA Action
 begin
 
 type_synonym
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/HOLCF/IOA/ABP/Receiver.thy
--- a/src/HOL/HOLCF/IOA/ABP/Receiver.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/HOLCF/IOA/ABP/Receiver.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>The implementation: receiver\<close>
 
 theory Receiver
-imports "../IOA" Action Lemmas
+imports IOA.IOA Action Lemmas
 begin
 
 type_synonym
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/HOLCF/IOA/ABP/Sender.thy
--- a/src/HOL/HOLCF/IOA/ABP/Sender.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/HOLCF/IOA/ABP/Sender.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>The implementation: sender\<close>
 
 theory Sender
-imports "../IOA" Action Lemmas
+imports IOA.IOA Action Lemmas
 begin
 
 type_synonym
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/HOLCF/IOA/ABP/Spec.thy
--- a/src/HOL/HOLCF/IOA/ABP/Spec.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/HOLCF/IOA/ABP/Spec.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>The specification of reliable transmission\<close>
 
 theory Spec
-imports "../IOA" Action
+imports IOA.IOA Action
 begin
 
 definition
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/HOLCF/IOA/NTP/Abschannel.thy
--- a/src/HOL/HOLCF/IOA/NTP/Abschannel.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/HOLCF/IOA/NTP/Abschannel.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>The (faulty) transmission channel (both directions)\<close>
 
 theory Abschannel
-imports "../IOA" Action
+imports IOA.IOA Action
 begin
 
 datatype 'a abs_action = S 'a | R 'a
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/HOLCF/IOA/NTP/Receiver.thy
--- a/src/HOL/HOLCF/IOA/NTP/Receiver.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/HOLCF/IOA/NTP/Receiver.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>The implementation: receiver\<close>
 
 theory Receiver
-imports "../IOA" Action
+imports IOA.IOA Action
 begin
 
 type_synonym
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/HOLCF/IOA/NTP/Sender.thy
--- a/src/HOL/HOLCF/IOA/NTP/Sender.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/HOLCF/IOA/NTP/Sender.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>The implementation: sender\<close>
 
 theory Sender
-imports "../IOA" Action
+imports IOA.IOA Action
 begin
 
 type_synonym
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/HOLCF/IOA/NTP/Spec.thy
--- a/src/HOL/HOLCF/IOA/NTP/Spec.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/HOLCF/IOA/NTP/Spec.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>The specification of reliable transmission\<close>
 
 theory Spec
-imports "../IOA" Action
+imports IOA.IOA Action
 begin
 
 definition
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/HOLCF/IOA/Seq.thy
--- a/src/HOL/HOLCF/IOA/Seq.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/HOLCF/IOA/Seq.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Partial, Finite and Infinite Sequences (lazy lists), modeled as domain\<close>
 
 theory Seq
-imports "../HOLCF"
+imports HOLCF
 begin
 
 default_sort pcpo
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/HOLCF/IOA/Storage/Correctness.thy
--- a/src/HOL/HOLCF/IOA/Storage/Correctness.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/HOLCF/IOA/Storage/Correctness.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Correctness Proof\<close>
 
 theory Correctness
-imports "../SimCorrectness" Spec Impl
+imports IOA.SimCorrectness Spec Impl
 begin
 
 default_sort type
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/HOLCF/IOA/Storage/Impl.thy
--- a/src/HOL/HOLCF/IOA/Storage/Impl.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/HOLCF/IOA/Storage/Impl.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>The implementation of a memory\<close>
 
 theory Impl
-imports "../IOA" Action
+imports IOA.IOA Action
 begin
 
 definition
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/HOLCF/IOA/Storage/Spec.thy
--- a/src/HOL/HOLCF/IOA/Storage/Spec.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/HOLCF/IOA/Storage/Spec.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>The specification of a memory\<close>
 
 theory Spec
-imports "../IOA" Action
+imports IOA.IOA Action
 begin
 
 definition
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/HOLCF/IOA/ex/TrivEx.thy
--- a/src/HOL/HOLCF/IOA/ex/TrivEx.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/HOLCF/IOA/ex/TrivEx.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Trivial Abstraction Example\<close>
 
 theory TrivEx
-imports "../Abstraction"
+imports IOA.Abstraction
 begin
 
 datatype action = INC
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/HOLCF/IOA/ex/TrivEx2.thy
--- a/src/HOL/HOLCF/IOA/ex/TrivEx2.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/HOLCF/IOA/ex/TrivEx2.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Trivial Abstraction Example with fairness\<close>
 
 theory TrivEx2
-imports "../Abstraction"
+imports IOA.Abstraction
 begin
 
 datatype action = INC
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/HOLCF/Library/Defl_Bifinite.thy
--- a/src/HOL/HOLCF/Library/Defl_Bifinite.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/HOLCF/Library/Defl_Bifinite.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Algebraic deflations are a bifinite domain\<close>
 
 theory Defl_Bifinite
-imports HOLCF "~~/src/HOL/Library/Infinite_Set"
+imports HOLCF "HOL-Library.Infinite_Set"
 begin
 
 subsection \<open>Lemmas about MOST\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/HOLCF/Library/Stream.thy
--- a/src/HOL/HOLCF/Library/Stream.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/HOLCF/Library/Stream.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>General Stream domain\<close>
 
 theory Stream
-imports "../HOLCF" "~~/src/HOL/Library/Extended_Nat"
+imports HOLCF "HOL-Library.Extended_Nat"
 begin
 
 default_sort pcpo
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/HOLCF/Representable.thy
--- a/src/HOL/HOLCF/Representable.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/HOLCF/Representable.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Representable domains\<close>
 
 theory Representable
-imports Algebraic Map_Functions "~~/src/HOL/Library/Countable"
+imports Algebraic Map_Functions "HOL-Library.Countable"
 begin
 
 default_sort cpo
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/HOLCF/Universal.thy
--- a/src/HOL/HOLCF/Universal.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/HOLCF/Universal.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>A universal bifinite domain\<close>
 
 theory Universal
-imports Bifinite Completion "~~/src/HOL/Library/Nat_Bijection"
+imports Bifinite Completion "HOL-Library.Nat_Bijection"
 begin
 
 no_notation binomial  (infixl "choose" 65)
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/HOLCF/ex/Dagstuhl.thy
--- a/src/HOL/HOLCF/ex/Dagstuhl.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/HOLCF/ex/Dagstuhl.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,5 +1,5 @@
 theory Dagstuhl
-imports "~~/src/HOL/HOLCF/Library/Stream"
+imports "HOLCF-Library.Stream"
 begin
 
 axiomatization
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/HOLCF/ex/Focus_ex.thy
--- a/src/HOL/HOLCF/ex/Focus_ex.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/HOLCF/ex/Focus_ex.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -99,7 +99,7 @@
 *)
 
 theory Focus_ex
-imports "~~/src/HOL/HOLCF/Library/Stream"
+imports "HOLCF-Library.Stream"
 begin
 
 typedecl ('a, 'b) tc
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Hahn_Banach/Bounds.thy
--- a/src/HOL/Hahn_Banach/Bounds.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Hahn_Banach/Bounds.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Bounds\<close>
 
 theory Bounds
-imports Main "~~/src/HOL/Analysis/Continuum_Not_Denumerable"
+imports Main "HOL-Analysis.Continuum_Not_Denumerable"
 begin
 
 locale lub =
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Hahn_Banach/Subspace.thy
--- a/src/HOL/Hahn_Banach/Subspace.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Hahn_Banach/Subspace.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Subspaces\<close>
 
 theory Subspace
-imports Vector_Space "~~/src/HOL/Library/Set_Algebras"
+imports Vector_Space "HOL-Library.Set_Algebras"
 begin
 
 subsection \<open>Definition\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/IMP/Abs_Int_init.thy
--- a/src/HOL/IMP/Abs_Int_init.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/IMP/Abs_Int_init.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,6 +1,6 @@
 theory Abs_Int_init
-imports "~~/src/HOL/Library/While_Combinator"
-        "~~/src/HOL/Library/Extended"
+imports "HOL-Library.While_Combinator"
+        "HOL-Library.Extended"
         Vars Collecting Abs_Int_Tests
 begin
 
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/IMP/Live_True.thy
--- a/src/HOL/IMP/Live_True.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/IMP/Live_True.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,7 +1,7 @@
 (* Author: Tobias Nipkow *)
 
 theory Live_True
-imports "~~/src/HOL/Library/While_Combinator" Vars Big_Step
+imports "HOL-Library.While_Combinator" Vars Big_Step
 begin
 
 subsection "True Liveness Analysis"
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Imperative_HOL/Heap.thy
--- a/src/HOL/Imperative_HOL/Heap.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Imperative_HOL/Heap.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>A polymorphic heap based on cantor encodings\<close>
 
 theory Heap
-imports Main "~~/src/HOL/Library/Countable"
+imports Main "HOL-Library.Countable"
 begin
 
 subsection \<open>Representable types\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -7,7 +7,7 @@
 theory Heap_Monad
 imports
   Heap
-  "~~/src/HOL/Library/Monad_Syntax"
+  "HOL-Library.Monad_Syntax"
 begin
 
 subsection \<open>The monad\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Imperative_HOL/Overview.thy
--- a/src/HOL/Imperative_HOL/Overview.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Imperative_HOL/Overview.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -4,7 +4,7 @@
 
 (*<*)
 theory Overview
-imports Imperative_HOL "~~/src/HOL/Library/LaTeXsugar"
+imports Imperative_HOL "HOL-Library.LaTeXsugar"
 begin
 
 (* type constraints with spacing *)
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -8,8 +8,8 @@
 imports
   "~~/src/HOL/Imperative_HOL/Imperative_HOL"
   Subarray
-  "~~/src/HOL/Library/Multiset"
-  "~~/src/HOL/Library/Code_Target_Numeral"
+  "HOL-Library.Multiset"
+  "HOL-Library.Code_Target_Numeral"
 begin
 
 text \<open>We prove QuickSort correct in the Relational Calculus.\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Imperative_HOL/ex/Linked_Lists.thy
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Linked Lists by ML references\<close>
 
 theory Linked_Lists
-imports "../Imperative_HOL" "~~/src/HOL/Library/Code_Target_Int"
+imports "../Imperative_HOL" "HOL-Library.Code_Target_Int"
 begin
 
 section \<open>Definition of Linked Lists\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Imperative_HOL/ex/List_Sublist.thy
--- a/src/HOL/Imperative_HOL/ex/List_Sublist.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Imperative_HOL/ex/List_Sublist.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Slices of lists\<close>
 
 theory List_Sublist
-imports "~~/src/HOL/Library/Multiset"
+imports "HOL-Library.Multiset"
 begin
 
 lemma nths_split: "i \<le> j \<and> j \<le> k \<Longrightarrow> nths xs {i..<j} @ nths xs {j..<k} = nths xs {i..<k}" 
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Imperative_HOL/ex/SatChecker.thy
--- a/src/HOL/Imperative_HOL/ex/SatChecker.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>An efficient checker for proofs from a SAT solver\<close>
 
 theory SatChecker
-imports "~~/src/HOL/Library/RBT_Impl" Sorted_List "../Imperative_HOL"
+imports "HOL-Library.RBT_Impl" Sorted_List "../Imperative_HOL"
 begin
 
 section\<open>General settings and functions for our representation of clauses\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Induct/Sexp.thy
--- a/src/HOL/Induct/Sexp.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Induct/Sexp.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -7,7 +7,7 @@
 *)
 
 theory Sexp
-imports "~~/src/HOL/Library/Old_Datatype"
+imports "HOL-Library.Old_Datatype"
 begin
 
 type_synonym 'a item = "'a Old_Datatype.item"
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Isar_Examples/Fibonacci.thy
--- a/src/HOL/Isar_Examples/Fibonacci.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Isar_Examples/Fibonacci.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -15,7 +15,7 @@
 section \<open>Fib and Gcd commute\<close>
 
 theory Fibonacci
-  imports "../Computational_Algebra/Primes"
+  imports "HOL-Computational_Algebra.Primes"
 begin
 
 text_raw \<open>\<^footnote>\<open>Isar version by Gertrud Bauer. Original tactic script by Larry
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Isar_Examples/Knaster_Tarski.thy
--- a/src/HOL/Isar_Examples/Knaster_Tarski.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Isar_Examples/Knaster_Tarski.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -7,7 +7,7 @@
 section \<open>Textbook-style reasoning: the Knaster-Tarski Theorem\<close>
 
 theory Knaster_Tarski
-  imports Main "~~/src/HOL/Library/Lattice_Syntax"
+  imports Main "HOL-Library.Lattice_Syntax"
 begin
 
 
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Library/Countable.thy
--- a/src/HOL/Library/Countable.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Library/Countable.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -7,7 +7,7 @@
 section \<open>Encoding (almost) everything into natural numbers\<close>
 
 theory Countable
-imports Old_Datatype "~~/src/HOL/Rat" Nat_Bijection
+imports Old_Datatype HOL.Rat Nat_Bijection
 begin
 
 subsection \<open>The class of countable types\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Library/Countable_Set_Type.thy
--- a/src/HOL/Library/Countable_Set_Type.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Library/Countable_Set_Type.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -9,7 +9,7 @@
 section \<open>Type of (at Most) Countable Sets\<close>
 
 theory Countable_Set_Type
-imports Countable_Set Cardinal_Notations Conditionally_Complete_Lattices
+imports Countable_Set Cardinal_Notations HOL.Conditionally_Complete_Lattices
 begin
 
 
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Library/FuncSet.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Pi and Function Sets\<close>
 
 theory FuncSet
-  imports Hilbert_Choice Main
+  imports HOL.Hilbert_Choice Main
   abbrevs PiE = "Pi\<^sub>E"
     PIE = "\<Pi>\<^sub>E"
 begin
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Library/Lattice_Syntax.thy
--- a/src/HOL/Library/Lattice_Syntax.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Library/Lattice_Syntax.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -3,7 +3,7 @@
 section \<open>Pretty syntax for lattice operations\<close>
 
 theory Lattice_Syntax
-imports Complete_Lattices
+imports HOL.Complete_Lattices
 begin
 
 notation
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Library/ListVector.thy
--- a/src/HOL/Library/ListVector.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Library/ListVector.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -3,7 +3,7 @@
 section \<open>Lists as vectors\<close>
 
 theory ListVector
-imports List Main
+imports HOL.List Main
 begin
 
 text\<open>\noindent
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Library/Option_ord.thy
--- a/src/HOL/Library/Option_ord.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Library/Option_ord.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Canonical order on option type\<close>
 
 theory Option_ord
-imports Option Main
+imports HOL.Option Main
 begin
 
 notation
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Library/Preorder.thy
--- a/src/HOL/Library/Preorder.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Library/Preorder.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -3,7 +3,7 @@
 section \<open>Preorders with explicit equivalence relation\<close>
 
 theory Preorder
-imports Orderings
+imports HOL.Orderings
 begin
 
 class preorder_equiv = preorder
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Matrix_LP/ComputeFloat.thy
--- a/src/HOL/Matrix_LP/ComputeFloat.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Matrix_LP/ComputeFloat.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Floating Point Representation of the Reals\<close>
 
 theory ComputeFloat
-imports Complex_Main "~~/src/HOL/Library/Lattice_Algebras"
+imports Complex_Main "HOL-Library.Lattice_Algebras"
 begin
 
 ML_file "~~/src/Tools/float.ML"
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Matrix_LP/Compute_Oracle/Compute_Oracle.thy
--- a/src/HOL/Matrix_LP/Compute_Oracle/Compute_Oracle.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Matrix_LP/Compute_Oracle/Compute_Oracle.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -4,7 +4,7 @@
 Steven Obua's evaluator.
 *)
 
-theory Compute_Oracle imports HOL
+theory Compute_Oracle imports HOL.HOL
 begin
 
 ML_file "am.ML"
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Matrix_LP/LP.thy
--- a/src/HOL/Matrix_LP/LP.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Matrix_LP/LP.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -3,7 +3,7 @@
 *)
 
 theory LP 
-imports Main "~~/src/HOL/Library/Lattice_Algebras"
+imports Main "HOL-Library.Lattice_Algebras"
 begin
 
 lemma le_add_right_mono: 
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Matrix_LP/Matrix.thy
--- a/src/HOL/Matrix_LP/Matrix.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Matrix_LP/Matrix.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -3,7 +3,7 @@
 *)
 
 theory Matrix
-imports Main "~~/src/HOL/Library/Lattice_Algebras"
+imports Main "HOL-Library.Lattice_Algebras"
 begin
 
 type_synonym 'a infmatrix = "nat \<Rightarrow> nat \<Rightarrow> 'a"
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Metis_Examples/Abstraction.thy
--- a/src/HOL/Metis_Examples/Abstraction.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Metis_Examples/Abstraction.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -8,7 +8,7 @@
 section \<open>Example Featuring Metis's Support for Lambda-Abstractions\<close>
 
 theory Abstraction
-imports "~~/src/HOL/Library/FuncSet"
+imports "HOL-Library.FuncSet"
 begin
 
 (* For Christoph Benzmüller *)
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Metis_Examples/Big_O.thy
--- a/src/HOL/Metis_Examples/Big_O.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Metis_Examples/Big_O.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -9,9 +9,9 @@
 
 theory Big_O
 imports
-  "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
-  "~~/src/HOL/Library/Function_Algebras"
-  "~~/src/HOL/Library/Set_Algebras"
+  "HOL-Decision_Procs.Dense_Linear_Order"
+  "HOL-Library.Function_Algebras"
+  "HOL-Library.Set_Algebras"
 begin
 
 subsection \<open>Definitions\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Metis_Examples/Tarski.thy
--- a/src/HOL/Metis_Examples/Tarski.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Metis_Examples/Tarski.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -8,7 +8,7 @@
 section \<open>Metis Example Featuring the Full Theorem of Tarski\<close>
 
 theory Tarski
-imports Main "~~/src/HOL/Library/FuncSet"
+imports Main "HOL-Library.FuncSet"
 begin
 
 declare [[metis_new_skolem]]
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/MicroJava/DFA/Kildall.thy
--- a/src/HOL/MicroJava/DFA/Kildall.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/MicroJava/DFA/Kildall.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -6,7 +6,7 @@
 section \<open>Kildall's Algorithm \label{sec:Kildall}\<close>
 
 theory Kildall
-imports SemilatAlg "~~/src/HOL/Library/While_Combinator"
+imports SemilatAlg "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 450cefec7c11 -r cc19f7ca2ed6 src/HOL/MicroJava/DFA/Semilat.thy
--- a/src/HOL/MicroJava/DFA/Semilat.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/MicroJava/DFA/Semilat.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -8,7 +8,7 @@
 section \<open>Semilattices\<close>
 
 theory Semilat
-imports Main "~~/src/HOL/Library/While_Combinator"
+imports Main "HOL-Library.While_Combinator"
 begin
 
 type_synonym 'a ord = "'a \<Rightarrow> 'a \<Rightarrow> bool"
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/MicroJava/J/JBasis.thy
--- a/src/HOL/MicroJava/J/JBasis.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/MicroJava/J/JBasis.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -9,8 +9,8 @@
 theory JBasis
 imports
   Main
-  "~~/src/HOL/Library/Transitive_Closure_Table"
-  "~~/src/HOL/Eisbach/Eisbach"
+  "HOL-Library.Transitive_Closure_Table"
+  "HOL-Eisbach.Eisbach"
 begin
 
 lemmas [simp] = Let_def
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Mutabelle/MutabelleExtra.thy
--- a/src/HOL/Mutabelle/MutabelleExtra.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Mutabelle/MutabelleExtra.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,5 +1,5 @@
 theory MutabelleExtra
-imports Complex_Main "~~/src/HOL/Library/Refute"
+imports Complex_Main "HOL-Library.Refute"
 (*  "~/repos/afp/thys/AVL-Trees/AVL"
   "~/repos/afp/thys/BinarySearchTree/BinaryTree"
   "~/repos/afp/thys/Huffman/Huffman"
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Nitpick_Examples/Manual_Nits.thy
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -12,7 +12,7 @@
    suite. *)
 
 theory Manual_Nits
-imports Real "~~/src/HOL/Library/Quotient_Product"
+imports HOL.Real "HOL-Library.Quotient_Product"
 begin
 
 section \<open>2. First Steps\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Nominal/Examples/CK_Machine.thy
--- a/src/HOL/Nominal/Examples/CK_Machine.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Nominal/Examples/CK_Machine.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,5 +1,5 @@
 theory CK_Machine 
-  imports "../Nominal" 
+  imports "HOL-Nominal.Nominal" 
 begin
 
 text \<open>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Nominal/Examples/CR_Takahashi.thy
--- a/src/HOL/Nominal/Examples/CR_Takahashi.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Nominal/Examples/CR_Takahashi.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -8,7 +8,7 @@
 (*  Church-Rosser Theorem (1995).                                 *)
 
 theory CR_Takahashi
-  imports "../Nominal"
+  imports "HOL-Nominal.Nominal"
 begin
 
 atom_decl name
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Nominal/Examples/Class1.thy
--- a/src/HOL/Nominal/Examples/Class1.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Nominal/Examples/Class1.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,5 +1,5 @@
 theory Class1
-imports "../Nominal" 
+imports "HOL-Nominal.Nominal" 
 begin
 
 section \<open>Term-Calculus from Urban's PhD\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Nominal/Examples/Compile.thy
--- a/src/HOL/Nominal/Examples/Compile.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Nominal/Examples/Compile.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,7 +1,7 @@
 (* The definitions for a challenge suggested by Adam Chlipala *)
 
 theory Compile
-imports "../Nominal"
+imports "HOL-Nominal.Nominal"
 begin
 
 atom_decl name 
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Nominal/Examples/Contexts.thy
--- a/src/HOL/Nominal/Examples/Contexts.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Nominal/Examples/Contexts.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,5 +1,5 @@
 theory Contexts
-imports "../Nominal"
+imports "HOL-Nominal.Nominal"
 begin
 
 text \<open>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Nominal/Examples/Crary.thy
--- a/src/HOL/Nominal/Examples/Crary.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Nominal/Examples/Crary.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -8,7 +8,7 @@
 (* Christian Urban.                                   *)
 
 theory Crary
-  imports "../Nominal"
+  imports "HOL-Nominal.Nominal"
 begin
 
 atom_decl name 
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Nominal/Examples/Fsub.thy
--- a/src/HOL/Nominal/Examples/Fsub.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Nominal/Examples/Fsub.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,6 +1,6 @@
 (*<*)
 theory Fsub
-imports "../Nominal" 
+imports "HOL-Nominal.Nominal" 
 begin
 (*>*)
 
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Nominal/Examples/Height.thy
--- a/src/HOL/Nominal/Examples/Height.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Nominal/Examples/Height.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,5 +1,5 @@
 theory Height
-  imports "../Nominal"
+  imports "HOL-Nominal.Nominal"
 begin
 
 text \<open>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Nominal/Examples/Lam_Funs.thy
--- a/src/HOL/Nominal/Examples/Lam_Funs.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Nominal/Examples/Lam_Funs.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,5 +1,5 @@
 theory Lam_Funs
-  imports "../Nominal"
+  imports "HOL-Nominal.Nominal"
 begin
 
 text \<open>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Nominal/Examples/Lambda_mu.thy
--- a/src/HOL/Nominal/Examples/Lambda_mu.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Nominal/Examples/Lambda_mu.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,5 +1,5 @@
 theory Lambda_mu 
-  imports "../Nominal" 
+  imports "HOL-Nominal.Nominal" 
 begin
 
 section \<open>Lambda-Mu according to a paper by Gavin Bierman\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Nominal/Examples/LocalWeakening.thy
--- a/src/HOL/Nominal/Examples/LocalWeakening.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Nominal/Examples/LocalWeakening.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -4,7 +4,7 @@
 (*                                                      *)
 (* Authors: Christian Urban and Randy Pollack           *)
 theory LocalWeakening
-  imports "../Nominal"
+  imports "HOL-Nominal.Nominal"
 begin
 
 atom_decl name
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Nominal/Examples/Pattern.thy
--- a/src/HOL/Nominal/Examples/Pattern.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Nominal/Examples/Pattern.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,7 +1,7 @@
 section \<open>Simply-typed lambda-calculus with let and tuple patterns\<close>
 
 theory Pattern
-imports "../Nominal"
+imports "HOL-Nominal.Nominal"
 begin
 
 no_syntax
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Nominal/Examples/SOS.thy
--- a/src/HOL/Nominal/Examples/SOS.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Nominal/Examples/SOS.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -11,7 +11,7 @@
 (* Christian Urban.                                       *)
 
 theory SOS
-  imports "../Nominal"
+  imports "HOL-Nominal.Nominal"
 begin
 
 atom_decl name
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Nominal/Examples/Standardization.thy
--- a/src/HOL/Nominal/Examples/Standardization.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Nominal/Examples/Standardization.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -6,7 +6,7 @@
 section \<open>Standardization\<close>
 
 theory Standardization
-imports "../Nominal"
+imports "HOL-Nominal.Nominal"
 begin
 
 text \<open>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Nominal/Examples/Support.thy
--- a/src/HOL/Nominal/Examples/Support.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Nominal/Examples/Support.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,5 +1,5 @@
 theory Support 
-  imports "../Nominal" 
+  imports "HOL-Nominal.Nominal" 
 begin
 
 text \<open>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Nominal/Examples/Type_Preservation.thy
--- a/src/HOL/Nominal/Examples/Type_Preservation.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Nominal/Examples/Type_Preservation.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,5 +1,5 @@
 theory Type_Preservation
-  imports "../Nominal"
+  imports "HOL-Nominal.Nominal"
 begin
 
 text \<open>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Nominal/Examples/VC_Condition.thy
--- a/src/HOL/Nominal/Examples/VC_Condition.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Nominal/Examples/VC_Condition.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,5 +1,5 @@
 theory VC_Condition
-imports "../Nominal" 
+imports "HOL-Nominal.Nominal" 
 begin
 
 text \<open>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Nominal/Examples/W.thy
--- a/src/HOL/Nominal/Examples/W.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Nominal/Examples/W.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,5 +1,5 @@
 theory W
-imports "../Nominal"
+imports "HOL-Nominal.Nominal"
 begin
 
 text \<open>Example for strong induction rules avoiding sets of atoms.\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Nominal/Examples/Weakening.thy
--- a/src/HOL/Nominal/Examples/Weakening.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Nominal/Examples/Weakening.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,5 +1,5 @@
 theory Weakening 
-  imports "../Nominal" 
+  imports "HOL-Nominal.Nominal" 
 begin
 
 text \<open>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,5 +1,5 @@
 theory Nominal 
-imports "~~/src/HOL/Library/Infinite_Set" "~~/src/HOL/Library/Old_Datatype"
+imports "HOL-Library.Infinite_Set" "HOL-Library.Old_Datatype"
 keywords
   "atom_decl" "nominal_datatype" "equivariance" :: thy_decl and
   "nominal_primrec" "nominal_inductive" "nominal_inductive2" :: thy_goal and
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy
--- a/src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -7,7 +7,7 @@
 section \<open>The Nonstandard Primes as an Extension of the Prime Numbers\<close>
 
 theory NSPrimes
-  imports "~~/src/HOL/Computational_Algebra/Primes" "../Hyperreal"
+  imports "HOL-Computational_Algebra.Primes" "HOL-Nonstandard_Analysis.Hyperreal"
 begin
 
 text \<open>These can be used to derive an alternative proof of the infinitude of
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Nonstandard_Analysis/Free_Ultrafilter.thy
--- a/src/HOL/Nonstandard_Analysis/Free_Ultrafilter.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Nonstandard_Analysis/Free_Ultrafilter.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -7,7 +7,7 @@
 section \<open>Filters and Ultrafilters\<close>
 
 theory Free_Ultrafilter
-  imports "~~/src/HOL/Library/Infinite_Set"
+  imports "HOL-Library.Infinite_Set"
 begin
 
 
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Nonstandard_Analysis/HSEQ.thy
--- a/src/HOL/Nonstandard_Analysis/HSEQ.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Nonstandard_Analysis/HSEQ.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -11,7 +11,7 @@
 section \<open>Sequences and Convergence (Nonstandard)\<close>
 
 theory HSEQ
-  imports Limits NatStar
+  imports HOL.Limits NatStar
   abbrevs "--->" = "\<longlonglongrightarrow>\<^sub>N\<^sub>S"
 begin
 
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Nonstandard_Analysis/HTranscendental.thy
--- a/src/HOL/Nonstandard_Analysis/HTranscendental.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Nonstandard_Analysis/HTranscendental.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -8,7 +8,7 @@
 section\<open>Nonstandard Extensions of Transcendental Functions\<close>
 
 theory HTranscendental
-imports Transcendental HSeries HDeriv
+imports HOL.Transcendental HSeries HDeriv
 begin
 
 definition
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Nonstandard_Analysis/NSA.thy
--- a/src/HOL/Nonstandard_Analysis/NSA.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Nonstandard_Analysis/NSA.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -6,7 +6,7 @@
 section \<open>Infinite Numbers, Infinitesimals, Infinitely Close Relation\<close>
 
 theory NSA
-  imports HyperDef "~~/src/HOL/Library/Lub_Glb"
+  imports HyperDef "HOL-Library.Lub_Glb"
 begin
 
 definition hnorm :: "'a::real_normed_vector star \<Rightarrow> real star"
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Number_Theory/Cong.thy
--- a/src/HOL/Number_Theory/Cong.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Number_Theory/Cong.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -29,7 +29,7 @@
 section \<open>Congruence\<close>
 
 theory Cong
-  imports "~~/src/HOL/Computational_Algebra/Primes"
+  imports "HOL-Computational_Algebra.Primes"
 begin
 
 subsection \<open>Turn off \<open>One_nat_def\<close>\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Number_Theory/Eratosthenes.thy
--- a/src/HOL/Number_Theory/Eratosthenes.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Number_Theory/Eratosthenes.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>The sieve of Eratosthenes\<close>
 
 theory Eratosthenes
-  imports Main "~~/src/HOL/Computational_Algebra/Primes"
+  imports Main "HOL-Computational_Algebra.Primes"
 begin
 
 
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Number_Theory/Prime_Powers.thy
--- a/src/HOL/Number_Theory/Prime_Powers.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Number_Theory/Prime_Powers.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -6,7 +6,7 @@
 *)
 section \<open>Prime powers\<close>
 theory Prime_Powers
-  imports Complex_Main "~~/src/HOL/Computational_Algebra/Primes"
+  imports Complex_Main "HOL-Computational_Algebra.Primes"
 begin
 
 definition aprimedivisor :: "'a :: normalization_semidom \<Rightarrow> 'a" where
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Number_Theory/Residues.thy
--- a/src/HOL/Number_Theory/Residues.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Number_Theory/Residues.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -10,10 +10,10 @@
 theory Residues
 imports
   Cong
-  "~~/src/HOL/Algebra/More_Group"
-  "~~/src/HOL/Algebra/More_Ring"
-  "~~/src/HOL/Algebra/More_Finite_Product"
-  "~~/src/HOL/Algebra/Multiplicative_Group"
+  "HOL-Algebra.More_Group"
+  "HOL-Algebra.More_Ring"
+  "HOL-Algebra.More_Finite_Product"
+  "HOL-Algebra.Multiplicative_Group"
   Totient
 begin
 
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Number_Theory/Totient.thy
--- a/src/HOL/Number_Theory/Totient.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Number_Theory/Totient.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -9,7 +9,7 @@
 theory Totient
 imports
   Complex_Main
-  "~~/src/HOL/Computational_Algebra/Primes"
+  "HOL-Computational_Algebra.Primes"
   "~~/src/HOL/Number_Theory/Cong"
 begin
   
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,5 +1,5 @@
 theory Code_Prolog_Examples
-imports "~~/src/HOL/Library/Code_Prolog"
+imports "HOL-Library.Code_Prolog"
 begin
 
 section \<open>Example append\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy
--- a/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,5 +1,5 @@
 theory Context_Free_Grammar_Example
-imports "~~/src/HOL/Library/Code_Prolog"
+imports "HOL-Library.Code_Prolog"
 begin
 (*
 declare mem_def[code_pred_inline]
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Predicate_Compile_Examples/Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Examples.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Examples.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,5 +1,5 @@
 theory Examples
-imports Main "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs"
+imports Main "HOL-Library.Predicate_Compile_Alternative_Defs"
 begin
 
 declare [[values_timeout = 480.0]]
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,8 +1,8 @@
 theory Hotel_Example_Prolog
 imports
   Hotel_Example
-  "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs"
-  "~~/src/HOL/Library/Code_Prolog"
+  "HOL-Library.Predicate_Compile_Alternative_Defs"
+  "HOL-Library.Code_Prolog"
 begin
 
 declare Let_def[code_pred_inline]
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Predicate_Compile_Examples/IMP_1.thy
--- a/src/HOL/Predicate_Compile_Examples/IMP_1.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Predicate_Compile_Examples/IMP_1.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,5 +1,5 @@
 theory IMP_1
-imports "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
+imports "HOL-Library.Predicate_Compile_Quickcheck"
 begin
 
 subsection \<open>IMP\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Predicate_Compile_Examples/IMP_2.thy
--- a/src/HOL/Predicate_Compile_Examples/IMP_2.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Predicate_Compile_Examples/IMP_2.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,5 +1,5 @@
 theory IMP_2
-imports "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
+imports "HOL-Library.Predicate_Compile_Quickcheck"
 begin
 
 subsection \<open>IMP\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Predicate_Compile_Examples/IMP_3.thy
--- a/src/HOL/Predicate_Compile_Examples/IMP_3.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Predicate_Compile_Examples/IMP_3.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,5 +1,5 @@
 theory IMP_3
-imports "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
+imports "HOL-Library.Predicate_Compile_Quickcheck"
 begin
 
 subsection \<open>IMP\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Predicate_Compile_Examples/IMP_4.thy
--- a/src/HOL/Predicate_Compile_Examples/IMP_4.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Predicate_Compile_Examples/IMP_4.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,5 +1,5 @@
 theory IMP_4
-imports "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
+imports "HOL-Library.Predicate_Compile_Quickcheck"
 begin
 
 subsection \<open>IMP\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Predicate_Compile_Examples/Lambda_Example.thy
--- a/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,5 +1,5 @@
 theory Lambda_Example
-imports "~~/src/HOL/Library/Code_Prolog"
+imports "HOL-Library.Code_Prolog"
 begin
 
 subsection \<open>Lambda\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Predicate_Compile_Examples/List_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/List_Examples.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Predicate_Compile_Examples/List_Examples.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,8 +1,8 @@
 theory List_Examples
 imports
   Main
-  "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
-  "~~/src/HOL/Library/Code_Prolog"
+  "HOL-Library.Predicate_Compile_Quickcheck"
+  "HOL-Library.Code_Prolog"
 begin
 
 setup \<open>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,5 +1,5 @@
 theory Predicate_Compile_Quickcheck_Examples
-imports "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
+imports "HOL-Library.Predicate_Compile_Quickcheck"
 begin
 
 (*
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,5 +1,5 @@
 theory Predicate_Compile_Tests
-imports "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs"
+imports "HOL-Library.Predicate_Compile_Alternative_Defs"
 begin
 
 declare [[values_timeout = 480.0]]
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy
--- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,7 +1,7 @@
 theory Reg_Exp_Example
 imports
-  "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
-  "~~/src/HOL/Library/Code_Prolog"
+  "HOL-Library.Predicate_Compile_Quickcheck"
+  "HOL-Library.Code_Prolog"
 begin
 
 text \<open>An example from the experiments from SmallCheck (\<^url>\<open>http://www.cs.york.ac.uk/fp/smallcheck\<close>)\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,5 +1,5 @@
 theory Specialisation_Examples
-imports Main "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs"
+imports Main "HOL-Library.Predicate_Compile_Alternative_Defs"
 begin
 
 declare [[values_timeout = 960.0]]
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Probability/Discrete_Topology.thy
--- a/src/HOL/Probability/Discrete_Topology.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Probability/Discrete_Topology.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -3,7 +3,7 @@
 *)
 
 theory Discrete_Topology
-imports "~~/src/HOL/Analysis/Analysis"
+imports "HOL-Analysis.Analysis"
 begin
 
 text \<open>Copy of discrete types with discrete topology. This space is polish.\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Probability/Essential_Supremum.thy
--- a/src/HOL/Probability/Essential_Supremum.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Probability/Essential_Supremum.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -4,7 +4,7 @@
 *)
 
 theory Essential_Supremum
-imports "../Analysis/Analysis"
+imports "HOL-Analysis.Analysis"
 begin
 
 lemma ae_filter_eq_bot_iff: "ae_filter M = bot \<longleftrightarrow> emeasure M (space M) = 0"
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Probability/Fin_Map.thy
--- a/src/HOL/Probability/Fin_Map.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Probability/Fin_Map.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Finite Maps\<close>
 
 theory Fin_Map
-  imports "~~/src/HOL/Analysis/Finite_Product_Measure" "~~/src/HOL/Library/Finite_Map"
+  imports "HOL-Analysis.Finite_Product_Measure" "HOL-Library.Finite_Map"
 begin
 
 text \<open>The @{type fmap} type can be instantiated to @{class polish_space}, needed for the proof of
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Probability/Giry_Monad.thy
--- a/src/HOL/Probability/Giry_Monad.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Probability/Giry_Monad.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -7,7 +7,7 @@
 *)
 
 theory Giry_Monad
-  imports Probability_Measure "~~/src/HOL/Library/Monad_Syntax"
+  imports Probability_Measure "HOL-Library.Monad_Syntax"
 begin
 
 section \<open>Sub-probability spaces\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Probability/Helly_Selection.thy
--- a/src/HOL/Probability/Helly_Selection.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Probability/Helly_Selection.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -8,7 +8,7 @@
 text \<open>The set of bounded, monotone, right continuous functions is sequentially compact\<close>
 
 theory Helly_Selection
-  imports "~~/src/HOL/Library/Diagonal_Subsequence" Weak_Convergence
+  imports "HOL-Library.Diagonal_Subsequence" Weak_Convergence
 begin
 
 lemma minus_one_less: "x - 1 < (x::real)"
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Probability/PMF_Impl.thy
--- a/src/HOL/Probability/PMF_Impl.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Probability/PMF_Impl.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -8,7 +8,7 @@
 section \<open>Code generation for PMFs\<close>
 
 theory PMF_Impl
-imports Probability_Mass_Function "~~/src/HOL/Library/AList_Mapping"
+imports Probability_Mass_Function "HOL-Library.AList_Mapping"
 begin
 
 subsection \<open>General code generation setup\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Probability/Probability_Mass_Function.thy
--- a/src/HOL/Probability/Probability_Mass_Function.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Probability/Probability_Mass_Function.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -8,7 +8,7 @@
 theory Probability_Mass_Function
 imports
   Giry_Monad
-  "~~/src/HOL/Library/Multiset"
+  "HOL-Library.Multiset"
 begin
 
 lemma AE_emeasure_singleton:
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Probability/Probability_Measure.thy
--- a/src/HOL/Probability/Probability_Measure.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Probability/Probability_Measure.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -6,7 +6,7 @@
 section \<open>Probability measure\<close>
 
 theory Probability_Measure
-  imports "~~/src/HOL/Analysis/Analysis"
+  imports "HOL-Analysis.Analysis"
 begin
 
 locale prob_space = finite_measure +
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Probability/Projective_Limit.thy
--- a/src/HOL/Probability/Projective_Limit.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Probability/Projective_Limit.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -8,7 +8,7 @@
 imports
   Fin_Map
   Infinite_Product_Measure
-  "~~/src/HOL/Library/Diagonal_Subsequence"
+  "HOL-Library.Diagonal_Subsequence"
 begin
 
 subsection \<open>Sequences of Finite Maps in Compact Sets\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Probability/Random_Permutations.thy
--- a/src/HOL/Probability/Random_Permutations.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Probability/Random_Permutations.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -13,7 +13,7 @@
 theory Random_Permutations
 imports 
   "~~/src/HOL/Probability/Probability_Mass_Function" 
-  "~~/src/HOL/Library/Multiset_Permutations"
+  "HOL-Library.Multiset_Permutations"
 begin
 
 text \<open>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Probability/SPMF.thy
--- a/src/HOL/Probability/SPMF.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Probability/SPMF.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -4,8 +4,8 @@
 
 theory SPMF imports
   Probability_Mass_Function
-  "~~/src/HOL/Library/Complete_Partial_Order2"
-  "~~/src/HOL/Library/Rewrite"
+  "HOL-Library.Complete_Partial_Order2"
+  "HOL-Library.Rewrite"
 begin
 
 subsection \<open>Auxiliary material\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Probability/Stopping_Time.thy
--- a/src/HOL/Probability/Stopping_Time.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Probability/Stopping_Time.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -3,7 +3,7 @@
 section {* Stopping times *}
 
 theory Stopping_Time
-  imports "../Analysis/Analysis"
+  imports "HOL-Analysis.Analysis"
 begin
 
 subsection \<open>Stopping Time\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Probability/Stream_Space.thy
--- a/src/HOL/Probability/Stream_Space.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Probability/Stream_Space.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -4,8 +4,8 @@
 theory Stream_Space
 imports
   Infinite_Product_Measure
-  "~~/src/HOL/Library/Stream"
-  "~~/src/HOL/Library/Linear_Temporal_Logic_on_Streams"
+  "HOL-Library.Stream"
+  "HOL-Library.Linear_Temporal_Logic_on_Streams"
 begin
 
 lemma stream_eq_Stream_iff: "s = x ## t \<longleftrightarrow> (shd s = x \<and> stl s = t)"
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Probability/Tree_Space.thy
--- a/src/HOL/Probability/Tree_Space.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Probability/Tree_Space.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -2,7 +2,7 @@
     Author:     Johannes Hölzl, CMU *)
 
 theory Tree_Space
-  imports Analysis "~~/src/HOL/Library/Tree"
+  imports "HOL-Analysis.Analysis" "HOL-Library.Tree"
 begin
 
 lemma countable_lfp:
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Probability/ex/Dining_Cryptographers.thy
--- a/src/HOL/Probability/ex/Dining_Cryptographers.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Probability/ex/Dining_Cryptographers.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,5 +1,5 @@
 theory Dining_Cryptographers
-imports "~~/src/HOL/Probability/Information"
+imports "HOL-Probability.Information"
 begin
 
 lemma image_ex1_eq: "inj_on f A \<Longrightarrow> (b \<in> f ` A) \<longleftrightarrow> (\<exists>!x \<in> A. b = f x)"
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy
--- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -3,7 +3,7 @@
 section \<open>Formalization of a Countermeasure by Koepf \& Duermuth 2009\<close>
 
 theory Koepf_Duermuth_Countermeasure
-  imports "~~/src/HOL/Probability/Information" "~~/src/HOL/Library/Permutation"
+  imports "HOL-Probability.Information" "HOL-Library.Permutation"
 begin
 
 lemma SIGMA_image_vimage:
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Probability/ex/Measure_Not_CCC.thy
--- a/src/HOL/Probability/ex/Measure_Not_CCC.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Probability/ex/Measure_Not_CCC.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -3,7 +3,7 @@
 section \<open>The Category of Measurable Spaces is not Cartesian Closed\<close>
 
 theory Measure_Not_CCC
-  imports "~~/src/HOL/Probability/Probability"
+  imports Probability
 begin
 
 text \<open>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Prolog/HOHH.thy
--- a/src/HOL/Prolog/HOHH.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Prolog/HOHH.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Higher-order hereditary Harrop formulas\<close>
 
 theory HOHH
-imports HOL
+imports HOL.HOL
 begin
 
 ML_file "prolog.ML"
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Proofs/Extraction/Euclid.thy
--- a/src/HOL/Proofs/Extraction/Euclid.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Proofs/Extraction/Euclid.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -8,10 +8,10 @@
 
 theory Euclid
 imports
-  "~~/src/HOL/Computational_Algebra/Primes"
+  "HOL-Computational_Algebra.Primes"
   Util
-  Old_Datatype
-  "~~/src/HOL/Library/Code_Target_Numeral"
+  "HOL-Library.Old_Datatype"
+  "HOL-Library.Code_Target_Numeral"
 begin
 
 text \<open>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Proofs/Extraction/Higman_Extraction.thy
--- a/src/HOL/Proofs/Extraction/Higman_Extraction.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Proofs/Extraction/Higman_Extraction.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -6,7 +6,7 @@
 subsection \<open>Extracting the program\<close>
 
 theory Higman_Extraction
-imports Higman Old_Datatype "~~/src/HOL/Library/Open_State_Syntax"
+imports Higman "HOL-Library.Old_Datatype" "HOL-Library.Open_State_Syntax"
 begin
 
 declare R.induct [ind_realizer]
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Proofs/Extraction/Pigeonhole.thy
--- a/src/HOL/Proofs/Extraction/Pigeonhole.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Proofs/Extraction/Pigeonhole.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>The pigeonhole principle\<close>
 
 theory Pigeonhole
-imports Util Old_Datatype "~~/src/HOL/Library/Code_Target_Numeral"
+imports Util "HOL-Library.Old_Datatype" "HOL-Library.Code_Target_Numeral"
 begin
 
 text \<open>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Proofs/Extraction/QuotRem.thy
--- a/src/HOL/Proofs/Extraction/QuotRem.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Proofs/Extraction/QuotRem.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Quotient and remainder\<close>
 
 theory QuotRem
-imports Old_Datatype Util
+imports "HOL-Library.Old_Datatype" Util
 begin
 
 text \<open>Derivation of quotient and remainder using program extraction.\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Proofs/Extraction/Warshall.thy
--- a/src/HOL/Proofs/Extraction/Warshall.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Proofs/Extraction/Warshall.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Warshall's algorithm\<close>
 
 theory Warshall
-imports Old_Datatype
+imports "HOL-Library.Old_Datatype"
 begin
 
 text \<open>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Proofs/ex/XML_Data.thy
--- a/src/HOL/Proofs/ex/XML_Data.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Proofs/ex/XML_Data.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -6,7 +6,7 @@
 *)
 
 theory XML_Data
-  imports "~~/src/HOL/Isar_Examples/Drinker"
+  imports "HOL-Isar_Examples.Drinker"
 begin
 
 subsection \<open>Export and re-import of global proof terms\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Quickcheck_Examples/Hotel_Example.thy
--- a/src/HOL/Quickcheck_Examples/Hotel_Example.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Quickcheck_Examples/Hotel_Example.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,5 +1,5 @@
 theory Hotel_Example
-imports Main "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
+imports Main "HOL-Library.Predicate_Compile_Quickcheck"
 begin
 
 datatype guest = Guest0 | Guest1
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy
--- a/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -6,7 +6,7 @@
 section \<open>Examples for the 'quickcheck' command\<close>
 
 theory Quickcheck_Examples
-imports Complex_Main "~~/src/HOL/Library/Dlist" "~~/src/HOL/Library/DAList_Multiset"
+imports Complex_Main "HOL-Library.Dlist" "HOL-Library.DAList_Multiset"
 begin
 
 text \<open>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Quotient_Examples/DList.thy
--- a/src/HOL/Quotient_Examples/DList.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Quotient_Examples/DList.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -8,7 +8,7 @@
 section \<open>Lists with distinct elements\<close>
 
 theory DList
-imports "~~/src/HOL/Library/Quotient_List"
+imports "HOL-Library.Quotient_List"
 begin
 
 text \<open>Some facts about lists\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Quotient_Examples/Int_Pow.thy
--- a/src/HOL/Quotient_Examples/Int_Pow.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Quotient_Examples/Int_Pow.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -4,7 +4,7 @@
 *)
 
 theory Int_Pow
-imports Main "~~/src/HOL/Algebra/Group"
+imports Main "HOL-Algebra.Group"
 begin
 
 (*
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Quotient_Examples/Lift_Fun.thy
--- a/src/HOL/Quotient_Examples/Lift_Fun.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Quotient_Examples/Lift_Fun.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -6,7 +6,7 @@
 
 
 theory Lift_Fun
-imports Main "~~/src/HOL/Library/Quotient_Syntax"
+imports Main "HOL-Library.Quotient_Syntax"
 begin
 
 text \<open>This file is meant as a test case. 
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Quotient_Examples/Quotient_FSet.thy
--- a/src/HOL/Quotient_Examples/Quotient_FSet.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_FSet.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -13,7 +13,7 @@
 *********************************************************************)
 
 theory Quotient_FSet
-imports "~~/src/HOL/Library/Multiset" "~~/src/HOL/Library/Quotient_List"
+imports "HOL-Library.Multiset" "HOL-Library.Quotient_List"
 begin
 
 text \<open>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Quotient_Examples/Quotient_Int.thy
--- a/src/HOL/Quotient_Examples/Quotient_Int.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_Int.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -7,7 +7,7 @@
 *)
 
 theory Quotient_Int
-imports "~~/src/HOL/Library/Quotient_Product" Nat
+imports "HOL-Library.Quotient_Product" HOL.Nat
 begin
 
 fun
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Quotient_Examples/Quotient_Message.thy
--- a/src/HOL/Quotient_Examples/Quotient_Message.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_Message.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 *)
 
 theory Quotient_Message
-imports Main "~~/src/HOL/Library/Quotient_Syntax"
+imports Main "HOL-Library.Quotient_Syntax"
 begin
 
 subsection\<open>Defining the Free Algebra\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Quotient_Examples/Quotient_Rat.thy
--- a/src/HOL/Quotient_Examples/Quotient_Rat.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_Rat.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -4,8 +4,8 @@
 Rational numbers defined with the quotient package, based on 'HOL/Rat.thy' by Makarius.
 *)
 
-theory Quotient_Rat imports Archimedean_Field
-  "~~/src/HOL/Library/Quotient_Product"
+theory Quotient_Rat imports HOL.Archimedean_Field
+  "HOL-Library.Quotient_Product"
 begin
 
 definition
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/ROOT
--- a/src/HOL/ROOT	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/ROOT	Fri Aug 18 20:47:47 2017 +0200
@@ -122,7 +122,7 @@
     mutually recursive relations.
   *}
   theories [document = false]
-    "~~/src/HOL/Library/Old_Datatype"
+    "HOL-Library.Old_Datatype"
   theories [quick_and_dirty]
     Common_Patterns
   theories
@@ -143,11 +143,11 @@
 session "HOL-IMP" (timing) in IMP = "HOL-Library" +
   options [document_variants = document]
   theories [document = false]
-    "~~/src/HOL/Library/While_Combinator"
-    "~~/src/HOL/Library/Char_ord"
-    "~~/src/HOL/Library/List_lexord"
-    "~~/src/HOL/Library/Quotient_List"
-    "~~/src/HOL/Library/Extended"
+    "HOL-Library.While_Combinator"
+    "HOL-Library.Char_ord"
+    "HOL-Library.List_lexord"
+    "HOL-Library.Quotient_List"
+    "HOL-Library.Extended"
   theories
     BExp
     ASM
@@ -200,8 +200,8 @@
     "HOL-Number_Theory"
   theories [document = false]
     Less_False
-    "~~/src/HOL/Library/Multiset"
-    "~~/src/HOL/Number_Theory/Fib"
+    "HOL-Library.Multiset"
+    "HOL-Number_Theory.Fib"
   theories
     Balance
     Tree_Map
@@ -228,10 +228,10 @@
   sessions
     "HOL-Algebra"
   theories [document = false]
-    "~~/src/HOL/Library/FuncSet"
-    "~~/src/HOL/Library/Multiset"
-    "~~/src/HOL/Algebra/Ring"
-    "~~/src/HOL/Algebra/FiniteProduct"
+    "HOL-Library.FuncSet"
+    "HOL-Library.Multiset"
+    "HOL-Algebra.Ring"
+    "HOL-Algebra.FiniteProduct"
   theories
     Number_Theory
   document_files
@@ -322,9 +322,9 @@
   *}
   theories [document = false]
     (* Preliminaries from set and number theory *)
-    "~~/src/HOL/Library/FuncSet"
-    "~~/src/HOL/Computational_Algebra/Primes"
-    "~~/src/HOL/Library/Permutation"
+    "HOL-Library.FuncSet"
+    "HOL-Computational_Algebra.Primes"
+    "HOL-Library.Permutation"
   theories
     (* Orders and Lattices *)
     Galois_Connection    (* Knaster-Tarski theorem and Galois connections *)
@@ -414,9 +414,9 @@
 session "HOL-Imperative_HOL" in Imperative_HOL = "HOL-Library" +
   options [print_mode = "iff,no_brackets"]
   theories [document = false]
-    "~~/src/HOL/Library/Countable"
-    "~~/src/HOL/Library/Monad_Syntax"
-    "~~/src/HOL/Library/LaTeXsugar"
+    "HOL-Library.Countable"
+    "HOL-Library.Monad_Syntax"
+    "HOL-Library.LaTeXsugar"
   theories Imperative_HOL_ex
   document_files "root.bib" "root.tex"
 
@@ -446,10 +446,10 @@
     "HOL-Library"
     "HOL-Computational_Algebra"
   theories [document = false]
-    "~~/src/HOL/Library/Code_Target_Numeral"
-    "~~/src/HOL/Library/Monad_Syntax"
-    "~~/src/HOL/Computational_Algebra/Primes"
-    "~~/src/HOL/Library/Open_State_Syntax"
+    "HOL-Library.Code_Target_Numeral"
+    "HOL-Library.Monad_Syntax"
+    "HOL-Computational_Algebra.Primes"
+    "HOL-Library.Open_State_Syntax"
   theories
     Greatest_Common_Divisor
     Warshall
@@ -501,7 +501,7 @@
   sessions
     "HOL-Eisbach"
   theories [document = false]
-    "~~/src/HOL/Library/While_Combinator"
+    "HOL-Library.While_Combinator"
   theories
     MicroJava
   document_files
@@ -664,8 +664,8 @@
   *}
   options [quick_and_dirty]
   theories [document = false]
-    "~~/src/HOL/Library/Lattice_Syntax"
-    "../Computational_Algebra/Primes"
+    "HOL-Library.Lattice_Syntax"
+    "HOL-Computational_Algebra.Primes"
   theories
     Knaster_Tarski
     Peirce
@@ -705,7 +705,7 @@
     Verification of the SET Protocol.
   *}
   theories [document = false]
-    "~~/src/HOL/Library/Nat_Bijection"
+    "HOL-Library.Nat_Bijection"
   theories
     SET_Protocol
   document_files "root.tex"
@@ -756,11 +756,11 @@
 
 session "HOL-Probability" (main timing) in "Probability" = "HOL-Analysis" +
   theories [document = false]
-    "~~/src/HOL/Library/Countable"
-    "~~/src/HOL/Library/Permutation"
-    "~~/src/HOL/Library/Order_Continuity"
-    "~~/src/HOL/Library/Diagonal_Subsequence"
-    "~~/src/HOL/Library/Finite_Map"
+    "HOL-Library.Countable"
+    "HOL-Library.Permutation"
+    "HOL-Library.Order_Continuity"
+    "HOL-Library.Diagonal_Subsequence"
+    "HOL-Library.Finite_Map"
   theories
     Probability (global)
   document_files "root.tex"
@@ -1084,8 +1084,8 @@
   sessions
     "HOL-Library"
   theories [document = false]
-    "~~/src/HOL/Library/Nat_Bijection"
-    "~~/src/HOL/Library/Countable"
+    "HOL-Library.Nat_Bijection"
+    "HOL-Library.Countable"
   theories
     HOLCF (global)
   document_files "root.tex"
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/SET_Protocol/Message_SET.thy
--- a/src/HOL/SET_Protocol/Message_SET.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/SET_Protocol/Message_SET.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -7,7 +7,7 @@
 section\<open>The Message Theory, Modified for SET\<close>
 
 theory Message_SET
-imports Main "~~/src/HOL/Library/Nat_Bijection"
+imports Main "HOL-Library.Nat_Bijection"
 begin
 
 subsection\<open>General Lemmas\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/SMT_Examples/SMT_Word_Examples.thy
--- a/src/HOL/SMT_Examples/SMT_Word_Examples.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/SMT_Examples/SMT_Word_Examples.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Word examples for for SMT binding\<close>
 
 theory SMT_Word_Examples
-imports "~~/src/HOL/Word/Word"
+imports "HOL-Word.Word"
 begin
 
 declare [[smt_oracle = true]]
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy
--- a/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -4,7 +4,7 @@
 *)
 
 theory Greatest_Common_Divisor
-imports "../../SPARK"
+imports SPARK
 begin
 
 spark_proof_functions
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy
--- a/src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -4,7 +4,7 @@
 *)
 
 theory Longest_Increasing_Subsequence
-imports "../../SPARK"
+imports SPARK
 begin
 
 text \<open>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/SPARK/Examples/RIPEMD-160/RMD.thy
--- a/src/HOL/SPARK/Examples/RIPEMD-160/RMD.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/RMD.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 *)
 
 theory RMD
-imports "~~/src/HOL/Word/Word"
+imports "HOL-Word.Word"
 begin
 
 
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/SPARK/Examples/RIPEMD-160/RMD_Specification.thy
--- a/src/HOL/SPARK/Examples/RIPEMD-160/RMD_Specification.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/RMD_Specification.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 *)
 
 theory RMD_Specification
-imports RMD "~~/src/HOL/SPARK/SPARK"
+imports RMD SPARK
 begin
 
 (* bit operations *)
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/SPARK/Examples/Sqrt/Sqrt.thy
--- a/src/HOL/SPARK/Examples/Sqrt/Sqrt.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/SPARK/Examples/Sqrt/Sqrt.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -4,7 +4,7 @@
 *)
 
 theory Sqrt
-imports "../../SPARK"
+imports SPARK
 begin
 
 spark_open "sqrt/isqrt"
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/SPARK/Manual/Complex_Types.thy
--- a/src/HOL/SPARK/Manual/Complex_Types.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/SPARK/Manual/Complex_Types.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,5 +1,5 @@
 theory Complex_Types
-imports "../SPARK"
+imports SPARK
 begin
 
 datatype day = Mon | Tue | Wed | Thu | Fri | Sat | Sun
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/SPARK/Manual/Example_Verification.thy
--- a/src/HOL/SPARK/Manual/Example_Verification.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/SPARK/Manual/Example_Verification.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,6 +1,6 @@
 (*<*)
 theory Example_Verification
-imports "../Examples/Gcd/Greatest_Common_Divisor" Simple_Greatest_Common_Divisor
+imports "HOL-SPARK-Examples.Greatest_Common_Divisor" Simple_Greatest_Common_Divisor
 begin
 (*>*)
 
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/SPARK/Manual/Proc1.thy
--- a/src/HOL/SPARK/Manual/Proc1.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/SPARK/Manual/Proc1.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,5 +1,5 @@
 theory Proc1
-imports "../SPARK"
+imports SPARK
 begin
 
 spark_open "loop_invariant/proc1"
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/SPARK/Manual/Proc2.thy
--- a/src/HOL/SPARK/Manual/Proc2.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/SPARK/Manual/Proc2.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,5 +1,5 @@
 theory Proc2
-imports "../SPARK"
+imports SPARK
 begin
 
 spark_open "loop_invariant/proc2"
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/SPARK/Manual/Reference.thy
--- a/src/HOL/SPARK/Manual/Reference.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/SPARK/Manual/Reference.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,6 +1,6 @@
 (*<*)
 theory Reference
-imports "../SPARK"
+imports SPARK
 begin
 
 syntax (my_constrain output)
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy
--- a/src/HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -4,7 +4,7 @@
 *)
 
 theory Simple_Greatest_Common_Divisor
-imports "../SPARK"
+imports SPARK
 begin
 
 spark_proof_functions
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/SPARK/SPARK_Setup.thy
--- a/src/HOL/SPARK/SPARK_Setup.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/SPARK/SPARK_Setup.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -6,7 +6,7 @@
 *)
 
 theory SPARK_Setup
-imports "~~/src/HOL/Word/Word" "~~/src/HOL/Word/Bit_Comparison"
+imports "HOL-Word.Word" "HOL-Word.Bit_Comparison"
 keywords
   "spark_open_vcg" :: thy_load ("vcg", "fdl", "rls") and
   "spark_open" :: thy_load ("siv", "fdl", "rls") and
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/TLA/Buffer/Buffer.thy
--- a/src/HOL/TLA/Buffer/Buffer.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/TLA/Buffer/Buffer.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>A simple FIFO buffer (synchronous communication, interleaving)\<close>
 
 theory Buffer
-imports "../TLA"
+imports "HOL-TLA.TLA"
 begin
 
 (* actions *)
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/TLA/Inc/Inc.thy
--- a/src/HOL/TLA/Inc/Inc.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/TLA/Inc/Inc.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Lamport's "increment" example\<close>
 
 theory Inc
-imports "../TLA"
+imports "HOL-TLA.TLA"
 begin
 
 (* program counter as an enumeration type *)
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/TLA/Memory/ProcedureInterface.thy
--- a/src/HOL/TLA/Memory/ProcedureInterface.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/TLA/Memory/ProcedureInterface.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Procedure interface for RPC-Memory components\<close>
 
 theory ProcedureInterface
-imports "../TLA" RPCMemoryParams
+imports "HOL-TLA.TLA" RPCMemoryParams
 begin
 
 typedecl ('a,'r) chan
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/TPTP/ATP_Problem_Import.thy
--- a/src/HOL/TPTP/ATP_Problem_Import.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/TPTP/ATP_Problem_Import.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>ATP Problem Importer\<close>
 
 theory ATP_Problem_Import
-imports Complex_Main TPTP_Interpret "~~/src/HOL/Library/Refute"
+imports Complex_Main TPTP_Interpret "HOL-Library.Refute"
 begin
 
 ML_file "sledgehammer_tactics.ML"
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/UNITY/Comp/AllocBase.thy
--- a/src/HOL/UNITY/Comp/AllocBase.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/UNITY/Comp/AllocBase.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 
 section\<open>Common Declarations for Chandy and Charpentier's Allocator\<close>
 
-theory AllocBase imports "../UNITY_Main" "~~/src/HOL/Library/Multiset_Order" begin
+theory AllocBase imports "../UNITY_Main" "HOL-Library.Multiset_Order" begin
 
 consts Nclients :: nat  (*Number of clients*)
 
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/UNITY/Follows.thy
--- a/src/HOL/UNITY/Follows.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/UNITY/Follows.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -6,7 +6,7 @@
 section\<open>The Follows Relation of Charpentier and Sivilotte\<close>
 
 theory Follows
-imports SubstAx ListOrder "~~/src/HOL/Library/Multiset"
+imports SubstAx ListOrder "HOL-Library.Multiset"
 begin
 
 definition Follows :: "['a => 'b::{order}, 'a => 'b::{order}] => 'a program set" (infixl "Fols" 65) where
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/UNITY/Simple/NSP_Bad.thy
--- a/src/HOL/UNITY/Simple/NSP_Bad.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/UNITY/Simple/NSP_Bad.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -7,7 +7,7 @@
 
 section\<open>Analyzing the Needham-Schroeder Public-Key Protocol in UNITY\<close>
 
-theory NSP_Bad imports "../../Auth/Public" "../UNITY_Main" begin
+theory NSP_Bad imports "HOL-Auth.Public" "../UNITY_Main" begin
 
 text\<open>This is the flawed version, vulnerable to Lowe's attack.
 From page 260 of
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Unix/Unix.thy
--- a/src/HOL/Unix/Unix.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Unix/Unix.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -7,7 +7,7 @@
 theory Unix
   imports
     Nested_Environment
-    "~~/src/HOL/Library/Sublist"
+    "HOL-Library.Sublist"
 begin
 
 text \<open>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Word/Bits_Bit.thy
--- a/src/HOL/Word/Bits_Bit.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Word/Bits_Bit.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Bit operations in $\cal Z_2$\<close>
 
 theory Bits_Bit
-imports Bits "~~/src/HOL/Library/Bit"
+imports Bits "HOL-Library.Bit"
 begin
 
 instantiation bit :: bit
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Word/Examples/WordExamples.thy
--- a/src/HOL/Word/Examples/WordExamples.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Word/Examples/WordExamples.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -7,7 +7,7 @@
 section "Examples of word operations"
 
 theory WordExamples
-  imports "../Word" "../WordBitwise"
+  imports "HOL-Word.Word" "HOL-Word.WordBitwise"
 begin
 
 type_synonym word32 = "32 word"
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Word/Word.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -6,8 +6,8 @@
 
 theory Word
 imports
-  "~~/src/HOL/Library/Type_Length"
-  "~~/src/HOL/Library/Boolean_Algebra"
+  "HOL-Library.Type_Length"
+  "HOL-Library.Boolean_Algebra"
   Bits_Bit
   Bool_List_Representation
   Misc_Typedef
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/Word/Word_Miscellaneous.thy
--- a/src/HOL/Word/Word_Miscellaneous.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Word/Word_Miscellaneous.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -3,7 +3,7 @@
 section \<open>Miscellaneous lemmas, of at least doubtful value\<close>
 
 theory Word_Miscellaneous
-  imports "~~/src/HOL/Library/Bit" Misc_Numeric
+  imports "HOL-Library.Bit" Misc_Numeric
 begin
 
 lemma power_minus_simp: "0 < n \<Longrightarrow> a ^ n = a * a ^ (n - 1)"
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/ZF/LProd.thy
--- a/src/HOL/ZF/LProd.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/ZF/LProd.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -6,7 +6,7 @@
 *)
 
 theory LProd 
-imports "~~/src/HOL/Library/Multiset"
+imports "HOL-Library.Multiset"
 begin
 
 inductive_set
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/ex/Adhoc_Overloading_Examples.thy
--- a/src/HOL/ex/Adhoc_Overloading_Examples.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/ex/Adhoc_Overloading_Examples.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -7,8 +7,8 @@
 theory Adhoc_Overloading_Examples
 imports
   Main
-  "~~/src/HOL/Library/Infinite_Set"
-  "~~/src/Tools/Adhoc_Overloading"
+  "HOL-Library.Infinite_Set"
+  "HOL-Library.Adhoc_Overloading"
 begin
 
 text \<open>Adhoc overloading allows to overload a constant depending on
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/ex/Ballot.thy
--- a/src/HOL/ex/Ballot.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/ex/Ballot.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -8,7 +8,7 @@
 theory Ballot
 imports
   Complex_Main
-  "~~/src/HOL/Library/FuncSet"
+  "HOL-Library.FuncSet"
 begin
 
 subsection \<open>Preliminaries\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/ex/Birthday_Paradox.thy
--- a/src/HOL/ex/Birthday_Paradox.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/ex/Birthday_Paradox.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>A Formulation of the Birthday Paradox\<close>
 
 theory Birthday_Paradox
-imports Main "~~/src/HOL/Binomial" "~~/src/HOL/Library/FuncSet"
+imports Main HOL.Binomial "HOL-Library.FuncSet"
 begin
 
 section \<open>Cardinality\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/ex/Bubblesort.thy
--- a/src/HOL/ex/Bubblesort.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/ex/Bubblesort.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -3,7 +3,7 @@
 section \<open>Bubblesort\<close>
 
 theory Bubblesort
-imports "~~/src/HOL/Library/Multiset"
+imports "HOL-Library.Multiset"
 begin
 
 text\<open>This is \emph{a} version of bubblesort.\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/ex/Code_Binary_Nat_examples.thy
--- a/src/HOL/ex/Code_Binary_Nat_examples.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/ex/Code_Binary_Nat_examples.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Simple examples for natural numbers implemented in binary representation.\<close>
 
 theory Code_Binary_Nat_examples
-imports Complex_Main "~~/src/HOL/Library/Code_Binary_Nat"
+imports Complex_Main "HOL-Library.Code_Binary_Nat"
 begin
 
 fun to_n :: "nat \<Rightarrow> nat list"
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/ex/Code_Timing.thy
--- a/src/HOL/ex/Code_Timing.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/ex/Code_Timing.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Examples for code generation timing measures\<close>
 
 theory Code_Timing
-imports "~~/src/HOL/Number_Theory/Eratosthenes"
+imports "HOL-Number_Theory.Eratosthenes"
 begin
 
 declare [[code_timing]]
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/ex/Computations.thy
--- a/src/HOL/ex/Computations.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/ex/Computations.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Simple example for computations generated by the code generator\<close>
 
 theory Computations
-  imports "../Nat" "../Fun_Def" "../Num" "../Code_Numeral"
+  imports HOL.Nat HOL.Fun_Def HOL.Num HOL.Code_Numeral
 begin
 
 fun even :: "nat \<Rightarrow> bool"
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/ex/Execute_Choice.thy
--- a/src/HOL/ex/Execute_Choice.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/ex/Execute_Choice.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -3,7 +3,7 @@
 section \<open>A simple cookbook example how to eliminate choice in programs.\<close>
 
 theory Execute_Choice
-imports Main "~~/src/HOL/Library/AList_Mapping"
+imports Main "HOL-Library.AList_Mapping"
 begin
 
 text \<open>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/ex/Functions.thy
--- a/src/HOL/ex/Functions.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/ex/Functions.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Examples of function definitions\<close>
 
 theory Functions
-imports Main "~~/src/HOL/Library/Monad_Syntax"
+imports Main "HOL-Library.Monad_Syntax"
 begin
 
 subsection \<open>Very basic\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/ex/Groebner_Examples.thy
--- a/src/HOL/ex/Groebner_Examples.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/ex/Groebner_Examples.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Groebner Basis Examples\<close>
 
 theory Groebner_Examples
-imports "~~/src/HOL/Groebner_Basis"
+imports HOL.Groebner_Basis
 begin
 
 subsection \<open>Basic examples\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/ex/IArray_Examples.thy
--- a/src/HOL/ex/IArray_Examples.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/ex/IArray_Examples.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,5 +1,5 @@
 theory IArray_Examples
-imports "~~/src/HOL/Library/IArray" "~~/src/HOL/Library/Code_Target_Numeral"
+imports "HOL-Library.IArray" "HOL-Library.Code_Target_Numeral"
 begin
 
 lemma "IArray [True,False] !! 1 = False"
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/ex/MergeSort.thy
--- a/src/HOL/ex/MergeSort.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/ex/MergeSort.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -6,7 +6,7 @@
 section\<open>Merge Sort\<close>
 
 theory MergeSort
-imports "~~/src/HOL/Library/Multiset"
+imports "HOL-Library.Multiset"
 begin
 
 context linorder
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/ex/Parallel_Example.thy
--- a/src/HOL/ex/Parallel_Example.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/ex/Parallel_Example.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,7 +1,7 @@
 section \<open>A simple example demonstrating parallelism for code generated towards Isabelle/ML\<close>
 
 theory Parallel_Example
-imports Complex_Main "~~/src/HOL/Library/Parallel" "~~/src/HOL/Library/Debug"
+imports Complex_Main "HOL-Library.Parallel" "HOL-Library.Debug"
 begin
 
 subsection \<open>Compute-intensive examples.\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/ex/Perm_Fragments.thy
--- a/src/HOL/ex/Perm_Fragments.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/ex/Perm_Fragments.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -3,7 +3,7 @@
 section \<open>Fragments on permuations\<close>
 
 theory Perm_Fragments
-imports "~~/src/HOL/Library/Perm" "~~/src/HOL/Library/Dlist"
+imports "HOL-Library.Perm" "HOL-Library.Dlist"
 begin
 
 unbundle permutation_syntax
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/ex/PresburgerEx.thy
--- a/src/HOL/ex/PresburgerEx.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/ex/PresburgerEx.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Some examples for Presburger Arithmetic\<close>
 
 theory PresburgerEx
-imports Presburger
+imports HOL.Presburger
 begin
 
 lemma "\<And>m n ja ia. \<lbrakk>\<not> m \<le> j; \<not> (n::nat) \<le> i; (e::nat) \<noteq> 0; Suc j \<le> ja\<rbrakk> \<Longrightarrow> \<exists>m. \<forall>ja ia. m \<le> ja \<longrightarrow> (if j = ja \<and> i = ia then e else 0) = 0" by presburger
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/ex/Quicksort.thy
--- a/src/HOL/ex/Quicksort.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/ex/Quicksort.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Quicksort with function package\<close>
 
 theory Quicksort
-imports "~~/src/HOL/Library/Multiset"
+imports "HOL-Library.Multiset"
 begin
 
 context linorder
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/ex/Reflection_Examples.thy
--- a/src/HOL/ex/Reflection_Examples.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/ex/Reflection_Examples.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Examples for generic reflection and reification\<close>
 
 theory Reflection_Examples
-imports Complex_Main "~~/src/HOL/Library/Reflection"
+imports Complex_Main "HOL-Library.Reflection"
 begin
 
 text \<open>This theory presents two methods: reify and reflection\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/ex/Refute_Examples.thy
--- a/src/HOL/ex/Refute_Examples.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/ex/Refute_Examples.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -8,7 +8,7 @@
 section \<open>Examples for the 'refute' command\<close>
 
 theory Refute_Examples
-imports "~~/src/HOL/Library/Refute"
+imports "HOL-Library.Refute"
 begin
 
 refute_params [satsolver = "cdclite"]
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/ex/Rewrite_Examples.thy
--- a/src/HOL/ex/Rewrite_Examples.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/ex/Rewrite_Examples.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,5 +1,5 @@
 theory Rewrite_Examples
-imports Main "~~/src/HOL/Library/Rewrite"
+imports Main "HOL-Library.Rewrite"
 begin
 
 section \<open>The rewrite Proof Method by Example\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/ex/SOS.thy
--- a/src/HOL/ex/SOS.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/ex/SOS.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -6,7 +6,7 @@
 *)
 
 theory SOS
-imports "~~/src/HOL/Library/Sum_of_Squares"
+imports "HOL-Library.Sum_of_Squares"
 begin
 
 lemma "(3::real) * x + 7 * a < 4 & 3 < 2 * x \<Longrightarrow> a < 0"
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/ex/SOS_Cert.thy
--- a/src/HOL/ex/SOS_Cert.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/ex/SOS_Cert.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -6,7 +6,7 @@
 *)
 
 theory SOS_Cert
-imports "~~/src/HOL/Library/Sum_of_Squares"
+imports "HOL-Library.Sum_of_Squares"
 begin
 
 lemma "(3::real) * x + 7 * a < 4 \<and> 3 < 2 * x \<Longrightarrow> a < 0"
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/ex/Simps_Case_Conv_Examples.thy
--- a/src/HOL/ex/Simps_Case_Conv_Examples.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/ex/Simps_Case_Conv_Examples.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,5 +1,5 @@
 theory Simps_Case_Conv_Examples imports
-  "~~/src/HOL/Library/Simps_Case_Conv"
+  "HOL-Library.Simps_Case_Conv"
 begin
 
 section \<open>Tests for the Simps<->Case conversion tools\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/ex/Sqrt.thy
--- a/src/HOL/ex/Sqrt.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/ex/Sqrt.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Square roots of primes are irrational\<close>
 
 theory Sqrt
-imports Complex_Main "~~/src/HOL/Computational_Algebra/Primes"
+imports Complex_Main "HOL-Computational_Algebra.Primes"
 begin
 
 text \<open>The square root of any prime number (including 2) is irrational.\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/ex/Sqrt_Script.thy
--- a/src/HOL/ex/Sqrt_Script.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/ex/Sqrt_Script.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -6,7 +6,7 @@
 section \<open>Square roots of primes are irrational (script version)\<close>
 
 theory Sqrt_Script
-imports Complex_Main "~~/src/HOL/Computational_Algebra/Primes"
+imports Complex_Main "HOL-Computational_Algebra.Primes"
 begin
 
 text \<open>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/ex/Tarski.thy
--- a/src/HOL/ex/Tarski.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/ex/Tarski.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>The Full Theorem of Tarski\<close>
 
 theory Tarski
-imports Main "~~/src/HOL/Library/FuncSet"
+imports Main "HOL-Library.FuncSet"
 begin
 
 text \<open>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/ex/Termination.thy
--- a/src/HOL/ex/Termination.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/ex/Termination.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -6,7 +6,7 @@
 section \<open>Examples and regression tests for automated termination proofs\<close>
  
 theory Termination
-imports Main "~~/src/HOL/Library/Multiset"
+imports Main "HOL-Library.Multiset"
 begin
 
 subsection \<open>Manually giving termination relations using \<open>relation\<close> and
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/ex/ThreeDivides.thy
--- a/src/HOL/ex/ThreeDivides.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/ex/ThreeDivides.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Three Divides Theorem\<close>
 
 theory ThreeDivides
-imports Main "~~/src/HOL/Library/LaTeXsugar"
+imports Main "HOL-Library.LaTeXsugar"
 begin
 
 subsection \<open>Abstract\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/ex/Transfer_Debug.thy
--- a/src/HOL/ex/Transfer_Debug.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/ex/Transfer_Debug.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -2,7 +2,7 @@
     Author:     Ondřej Kunčar, TU München
 *)
 theory Transfer_Debug 
-imports Main "~~/src/HOL/Library/FSet"
+imports Main "HOL-Library.FSet"
 begin                              
 
 (*
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/ex/Transitive_Closure_Table_Ex.thy
--- a/src/HOL/ex/Transitive_Closure_Table_Ex.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/ex/Transitive_Closure_Table_Ex.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -3,7 +3,7 @@
 section \<open>Simple example for table-based implementation of the reflexive transitive closure\<close>
 
 theory Transitive_Closure_Table_Ex
-imports "~~/src/HOL/Library/Transitive_Closure_Table"
+imports "HOL-Library.Transitive_Closure_Table"
 begin
 
 datatype ty = A | B | C
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/ex/While_Combinator_Example.thy
--- a/src/HOL/ex/While_Combinator_Example.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/ex/While_Combinator_Example.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -6,7 +6,7 @@
 section \<open>An application of the While combinator\<close>
 
 theory While_Combinator_Example
-imports "~~/src/HOL/Library/While_Combinator"
+imports "HOL-Library.While_Combinator"
 begin
 
 text \<open>Computation of the @{term lfp} on finite sets via 
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/ex/Word_Type.thy
--- a/src/HOL/ex/Word_Type.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/ex/Word_Type.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -6,7 +6,7 @@
 theory Word_Type
   imports
     Main
-    "~~/src/HOL/Library/Type_Length"
+    "HOL-Library.Type_Length"
 begin
 
 subsection \<open>Truncating bit representations of numeric types\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/LCF/LCF.thy
--- a/src/LCF/LCF.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/LCF/LCF.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -6,7 +6,7 @@
 section \<open>LCF on top of First-Order Logic\<close>
 
 theory LCF
-imports "~~/src/FOL/FOL"
+imports FOL
 begin
 
 text \<open>This theory is based on Lawrence Paulson's book Logic and Computation.\<close>
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/ZF/UNITY/MultisetSum.thy
--- a/src/ZF/UNITY/MultisetSum.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/ZF/UNITY/MultisetSum.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Setsum for Multisets\<close>
 
 theory MultisetSum
-imports "../Induct/Multiset"
+imports "ZF-Induct.Multiset"
 begin
 
 definition
diff -r 450cefec7c11 -r cc19f7ca2ed6 src/ZF/ZF_Base.thy
--- a/src/ZF/ZF_Base.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/ZF/ZF_Base.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -6,7 +6,7 @@
 section \<open>Base of Zermelo-Fraenkel Set Theory\<close>
 
 theory ZF_Base
-imports "~~/src/FOL/FOL"
+imports FOL
 begin
 
 subsection \<open>Signature\<close>