merged
authorwenzelm
Fri Aug 18 22:55:54 2017 +0200 (21 months ago)
changeset 66455158c513a39f5
parent 66451 5be0b0604d71
parent 66454 1a73ad1c06dd
child 66456 621897f47fab
child 66457 9098c36abd1a
merged
NEWS
     1.1 --- a/NEWS	Fri Aug 18 14:57:23 2017 +0200
     1.2 +++ b/NEWS	Fri Aug 18 22:55:54 2017 +0200
     1.3 @@ -23,14 +23,22 @@
     1.4  modules around a Language Server implementation.
     1.5  
     1.6  * Theory names are qualified by the session name that they belong to.
     1.7 -This affects imports, but not the theory name space prefix: it remains
     1.8 -the theory base name as before. In order to import theories from other
     1.9 -sessions, the ROOT file format provides a new 'sessions' keyword. In
    1.10 -contrast, a theory that is imported in the old-fashioned manner via an
    1.11 -explicit file-system path belongs to the current session.
    1.12 -
    1.13 -Theories that are imported from other sessions are excluded from the
    1.14 -current session document.
    1.15 +This affects imports, but not the theory name space prefix (which is
    1.16 +just the theory base name as before).
    1.17 +
    1.18 +In order to import theories from other sessions, the ROOT file format
    1.19 +provides a new 'sessions' keyword. In contrast, a theory that is
    1.20 +imported in the old-fashioned manner via an explicit file-system path
    1.21 +belongs to the current session, and might cause theory name confusion
    1.22 +later on. Theories that are imported from other sessions are excluded
    1.23 +from the current session document. The command-line tool "isabelle
    1.24 +imports" helps to update theory imports.
    1.25 +
    1.26 +Properly qualified imports allow the Prover IDE to process arbitrary
    1.27 +theory hierarchies independently of the underlying logic session image
    1.28 +(e.g. option "isabelle jedit -l"), but the directory structure needs to
    1.29 +be known in advance (e.g. option "isabelle jedit -d" or a line in the
    1.30 +file $ISABELLE_HOME_USER/ROOTS).
    1.31  
    1.32  * The main theory entry points for some non-HOL sessions have changed,
    1.33  to avoid confusion with the global name "Main" of the session HOL. This
     2.1 --- a/src/Benchmarks/Datatype_Benchmark/IsaFoR.thy	Fri Aug 18 14:57:23 2017 +0200
     2.2 +++ b/src/Benchmarks/Datatype_Benchmark/IsaFoR.thy	Fri Aug 18 22:55:54 2017 +0200
     2.3 @@ -8,7 +8,7 @@
     2.4  section \<open>Benchmark Consisting of Datatypes Defined in IsaFoR\<close>
     2.5  
     2.6  theory IsaFoR
     2.7 -imports Real
     2.8 +imports HOL.Real
     2.9  begin
    2.10  
    2.11  datatype (discs_sels) ('f, 'l) lab =
     3.1 --- a/src/Benchmarks/Datatype_Benchmark/Misc_N2M.thy	Fri Aug 18 14:57:23 2017 +0200
     3.2 +++ b/src/Benchmarks/Datatype_Benchmark/Misc_N2M.thy	Fri Aug 18 22:55:54 2017 +0200
     3.3 @@ -8,7 +8,7 @@
     3.4  section \<open>Miscellaneous Tests for the Nested-to-Mutual Reduction\<close>
     3.5  
     3.6  theory Misc_N2M
     3.7 -imports "~~/src/HOL/Library/BNF_Axiomatization"
     3.8 +imports "HOL-Library.BNF_Axiomatization"
     3.9  begin
    3.10  
    3.11  declare [[typedef_overloaded]]
     4.1 --- a/src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy	Fri Aug 18 14:57:23 2017 +0200
     4.2 +++ b/src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy	Fri Aug 18 22:55:54 2017 +0200
     4.3 @@ -1,5 +1,5 @@
     4.4  theory Needham_Schroeder_Base
     4.5 -imports Main "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
     4.6 +imports Main "HOL-Library.Predicate_Compile_Quickcheck"
     4.7  begin
     4.8  
     4.9  datatype agent = Alice | Bob | Spy
     5.1 --- a/src/CCL/Set.thy	Fri Aug 18 14:57:23 2017 +0200
     5.2 +++ b/src/CCL/Set.thy	Fri Aug 18 22:55:54 2017 +0200
     5.3 @@ -1,7 +1,7 @@
     5.4  section \<open>Extending FOL by a modified version of HOL set theory\<close>
     5.5  
     5.6  theory Set
     5.7 -imports "~~/src/FOL/FOL"
     5.8 +imports FOL
     5.9  begin
    5.10  
    5.11  declare [[eta_contract]]
     6.1 --- a/src/Doc/Codegen/Adaptation.thy	Fri Aug 18 14:57:23 2017 +0200
     6.2 +++ b/src/Doc/Codegen/Adaptation.thy	Fri Aug 18 22:55:54 2017 +0200
     6.3 @@ -1,5 +1,5 @@
     6.4  theory Adaptation
     6.5 -imports Setup
     6.6 +imports Codegen_Basics.Setup
     6.7  begin
     6.8  
     6.9  setup %invisible \<open>Code_Target.add_derived_target ("\<SML>", [("SML", I)])
     7.1 --- a/src/Doc/Codegen/Computations.thy	Fri Aug 18 14:57:23 2017 +0200
     7.2 +++ b/src/Doc/Codegen/Computations.thy	Fri Aug 18 22:55:54 2017 +0200
     7.3 @@ -1,7 +1,7 @@
     7.4  theory Computations
     7.5 -  imports Setup
     7.6 -    "~~/src/HOL/Library/Code_Target_Int"
     7.7 -    "~~/src/HOL/Library/Code_Char"
     7.8 +  imports Codegen_Basics.Setup
     7.9 +    "HOL-Library.Code_Target_Int"
    7.10 +    "HOL-Library.Code_Char"
    7.11  begin
    7.12  
    7.13  section \<open>Computations \label{sec:computations}\<close>
     8.1 --- a/src/Doc/Codegen/Evaluation.thy	Fri Aug 18 14:57:23 2017 +0200
     8.2 +++ b/src/Doc/Codegen/Evaluation.thy	Fri Aug 18 22:55:54 2017 +0200
     8.3 @@ -1,5 +1,5 @@
     8.4  theory Evaluation
     8.5 -imports Setup
     8.6 +imports Codegen_Basics.Setup
     8.7  begin (*<*)
     8.8  
     8.9  ML \<open>
     9.1 --- a/src/Doc/Codegen/Further.thy	Fri Aug 18 14:57:23 2017 +0200
     9.2 +++ b/src/Doc/Codegen/Further.thy	Fri Aug 18 22:55:54 2017 +0200
     9.3 @@ -1,5 +1,5 @@
     9.4  theory Further
     9.5 -imports Setup
     9.6 +imports Codegen_Basics.Setup
     9.7  begin
     9.8  
     9.9  section \<open>Further issues \label{sec:further}\<close>
    10.1 --- a/src/Doc/Codegen/Inductive_Predicate.thy	Fri Aug 18 14:57:23 2017 +0200
    10.2 +++ b/src/Doc/Codegen/Inductive_Predicate.thy	Fri Aug 18 22:55:54 2017 +0200
    10.3 @@ -1,5 +1,5 @@
    10.4  theory Inductive_Predicate
    10.5 -imports Setup
    10.6 +imports Codegen_Basics.Setup
    10.7  begin
    10.8  
    10.9  (*<*)
    11.1 --- a/src/Doc/Codegen/Introduction.thy	Fri Aug 18 14:57:23 2017 +0200
    11.2 +++ b/src/Doc/Codegen/Introduction.thy	Fri Aug 18 22:55:54 2017 +0200
    11.3 @@ -1,5 +1,5 @@
    11.4  theory Introduction
    11.5 -imports Setup
    11.6 +imports Codegen_Basics.Setup
    11.7  begin (*<*)
    11.8  
    11.9  ML \<open>
    12.1 --- a/src/Doc/Codegen/Refinement.thy	Fri Aug 18 14:57:23 2017 +0200
    12.2 +++ b/src/Doc/Codegen/Refinement.thy	Fri Aug 18 22:55:54 2017 +0200
    12.3 @@ -1,5 +1,5 @@
    12.4  theory Refinement
    12.5 -imports Setup
    12.6 +imports Codegen_Basics.Setup
    12.7  begin
    12.8  
    12.9  section \<open>Program and datatype refinement \label{sec:refinement}\<close>
    13.1 --- a/src/Doc/Codegen/Setup.thy	Fri Aug 18 14:57:23 2017 +0200
    13.2 +++ b/src/Doc/Codegen/Setup.thy	Fri Aug 18 22:55:54 2017 +0200
    13.3 @@ -1,10 +1,10 @@
    13.4  theory Setup
    13.5  imports
    13.6    Complex_Main
    13.7 -  "~~/src/HOL/Library/Dlist"
    13.8 -  "~~/src/HOL/Library/RBT"
    13.9 -  "~~/src/HOL/Library/Mapping"
   13.10 -  "~~/src/HOL/Library/IArray"
   13.11 +  "HOL-Library.Dlist"
   13.12 +  "HOL-Library.RBT"
   13.13 +  "HOL-Library.Mapping"
   13.14 +  "HOL-Library.IArray"
   13.15  begin
   13.16  
   13.17  ML_file "../antiquote_setup.ML"
    14.1 --- a/src/Doc/Corec/Corec.thy	Fri Aug 18 14:57:23 2017 +0200
    14.2 +++ b/src/Doc/Corec/Corec.thy	Fri Aug 18 22:55:54 2017 +0200
    14.3 @@ -9,8 +9,8 @@
    14.4  *)
    14.5  
    14.6  theory Corec
    14.7 -imports Main "../Datatypes/Setup" "~~/src/HOL/Library/BNF_Corec"
    14.8 -  "~~/src/HOL/Library/FSet"
    14.9 +imports Main Datatypes.Setup "HOL-Library.BNF_Corec"
   14.10 +  "HOL-Library.FSet"
   14.11  begin
   14.12  
   14.13  section \<open>Introduction
    15.1 --- a/src/Doc/Datatypes/Datatypes.thy	Fri Aug 18 14:57:23 2017 +0200
    15.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Fri Aug 18 22:55:54 2017 +0200
    15.3 @@ -12,11 +12,11 @@
    15.4  theory Datatypes
    15.5  imports
    15.6    Setup
    15.7 -  "~~/src/HOL/Library/BNF_Axiomatization"
    15.8 -  "~~/src/HOL/Library/Cardinal_Notations"
    15.9 -  "~~/src/HOL/Library/Countable"
   15.10 -  "~~/src/HOL/Library/FSet"
   15.11 -  "~~/src/HOL/Library/Simps_Case_Conv"
   15.12 +  "HOL-Library.BNF_Axiomatization"
   15.13 +  "HOL-Library.Cardinal_Notations"
   15.14 +  "HOL-Library.Countable"
   15.15 +  "HOL-Library.FSet"
   15.16 +  "HOL-Library.Simps_Case_Conv"
   15.17  begin
   15.18  
   15.19  section \<open>Introduction
    16.1 --- a/src/Doc/Eisbach/Manual.thy	Fri Aug 18 14:57:23 2017 +0200
    16.2 +++ b/src/Doc/Eisbach/Manual.thy	Fri Aug 18 22:55:54 2017 +0200
    16.3 @@ -1,7 +1,7 @@
    16.4  (*:maxLineLen=78:*)
    16.5  
    16.6  theory Manual
    16.7 -imports Base "~~/src/HOL/Eisbach/Eisbach_Tools"
    16.8 +imports Base "HOL-Eisbach.Eisbach_Tools"
    16.9  begin
   16.10  
   16.11  chapter \<open>The method command\<close>
    17.1 --- a/src/Doc/Eisbach/Preface.thy	Fri Aug 18 14:57:23 2017 +0200
    17.2 +++ b/src/Doc/Eisbach/Preface.thy	Fri Aug 18 22:55:54 2017 +0200
    17.3 @@ -1,7 +1,7 @@
    17.4  (*:maxLineLen=78:*)
    17.5  
    17.6  theory Preface
    17.7 -imports Base "~~/src/HOL/Eisbach/Eisbach_Tools"
    17.8 +imports Base "HOL-Eisbach.Eisbach_Tools"
    17.9  begin
   17.10  
   17.11  text \<open>
    18.1 --- a/src/Doc/Isar_Ref/HOL_Specific.thy	Fri Aug 18 14:57:23 2017 +0200
    18.2 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Fri Aug 18 22:55:54 2017 +0200
    18.3 @@ -3,11 +3,11 @@
    18.4  theory HOL_Specific
    18.5    imports
    18.6      Main
    18.7 -    "~~/src/HOL/Library/Old_Datatype"
    18.8 -    "~~/src/HOL/Library/Old_Recdef"
    18.9 -    "~~/src/Tools/Adhoc_Overloading"
   18.10 -    "~~/src/HOL/Library/Dlist"
   18.11 -    "~~/src/HOL/Library/FSet"
   18.12 +    "HOL-Library.Old_Datatype"
   18.13 +    "HOL-Library.Old_Recdef"
   18.14 +    "HOL-Library.Adhoc_Overloading"
   18.15 +    "HOL-Library.Dlist"
   18.16 +    "HOL-Library.FSet"
   18.17      Base
   18.18  begin
   18.19  
    19.1 --- a/src/Doc/Logics_ZF/FOL_examples.thy	Fri Aug 18 14:57:23 2017 +0200
    19.2 +++ b/src/Doc/Logics_ZF/FOL_examples.thy	Fri Aug 18 22:55:54 2017 +0200
    19.3 @@ -1,6 +1,6 @@
    19.4  section{*Examples of Classical Reasoning*}
    19.5  
    19.6 -theory FOL_examples imports "~~/src/FOL/FOL" begin
    19.7 +theory FOL_examples imports FOL begin
    19.8  
    19.9  lemma "EX y. ALL x. P(y)-->P(x)"
   19.10    --{* @{subgoals[display,indent=0,margin=65]} *}
    20.1 --- a/src/Doc/Logics_ZF/IFOL_examples.thy	Fri Aug 18 14:57:23 2017 +0200
    20.2 +++ b/src/Doc/Logics_ZF/IFOL_examples.thy	Fri Aug 18 22:55:54 2017 +0200
    20.3 @@ -1,6 +1,6 @@
    20.4  section{*Examples of Intuitionistic Reasoning*}
    20.5  
    20.6 -theory IFOL_examples imports "~~/src/FOL/IFOL" begin
    20.7 +theory IFOL_examples imports IFOL begin
    20.8  
    20.9  text{*Quantifier example from the book Logic and Computation*}
   20.10  lemma "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
    21.1 --- a/src/Doc/Logics_ZF/If.thy	Fri Aug 18 14:57:23 2017 +0200
    21.2 +++ b/src/Doc/Logics_ZF/If.thy	Fri Aug 18 22:55:54 2017 +0200
    21.3 @@ -5,7 +5,7 @@
    21.4  First-Order Logic: the 'if' example.
    21.5  *)
    21.6  
    21.7 -theory If imports "~~/src/FOL/FOL" begin
    21.8 +theory If imports FOL begin
    21.9  
   21.10  definition "if" :: "[o,o,o]=>o" where
   21.11    "if(P,Q,R) == P&Q | ~P&R"
    22.1 --- a/src/Doc/ROOT	Fri Aug 18 14:57:23 2017 +0200
    22.2 +++ b/src/Doc/ROOT	Fri Aug 18 22:55:54 2017 +0200
    22.3 @@ -48,7 +48,7 @@
    22.4    options [document_variants = "corec"]
    22.5    sessions
    22.6      Datatypes
    22.7 -  theories [document = false] "../Datatypes/Setup"
    22.8 +  theories [document = false] Datatypes.Setup
    22.9    theories Corec
   22.10    document_files (in "..")
   22.11      "prepare_document"
   22.12 @@ -249,8 +249,8 @@
   22.13    sessions
   22.14      "HOL-Library"
   22.15    theories [document = false]
   22.16 -    "~~/src/HOL/Library/LaTeXsugar"
   22.17 -    "~~/src/HOL/Library/OptionalSugar"
   22.18 +    "HOL-Library.LaTeXsugar"
   22.19 +    "HOL-Library.OptionalSugar"
   22.20    theories Sugar
   22.21    document_files (in "..")
   22.22      "prepare_document"
    23.1 --- a/src/Doc/Sugar/Sugar.thy	Fri Aug 18 14:57:23 2017 +0200
    23.2 +++ b/src/Doc/Sugar/Sugar.thy	Fri Aug 18 22:55:54 2017 +0200
    23.3 @@ -1,8 +1,8 @@
    23.4  (*<*)
    23.5  theory Sugar
    23.6  imports
    23.7 -  "~~/src/HOL/Library/LaTeXsugar"
    23.8 -  "~~/src/HOL/Library/OptionalSugar"
    23.9 +  "HOL-Library.LaTeXsugar"
   23.10 +  "HOL-Library.OptionalSugar"
   23.11  begin
   23.12  no_translations
   23.13    ("prop") "P \<and> Q \<Longrightarrow> R" <= ("prop") "P \<Longrightarrow> Q \<Longrightarrow> R"
    24.1 --- a/src/Doc/Typeclass_Hierarchy/Setup.thy	Fri Aug 18 14:57:23 2017 +0200
    24.2 +++ b/src/Doc/Typeclass_Hierarchy/Setup.thy	Fri Aug 18 22:55:54 2017 +0200
    24.3 @@ -1,5 +1,5 @@
    24.4  theory Setup
    24.5 -imports Complex_Main "~~/src/HOL/Library/Multiset" "~~/src/HOL/Library/Lattice_Syntax"
    24.6 +imports Complex_Main "HOL-Library.Multiset" "HOL-Library.Lattice_Syntax"
    24.7  begin
    24.8  
    24.9  ML_file "../antiquote_setup.ML"
    25.1 --- a/src/Doc/Typeclass_Hierarchy/Typeclass_Hierarchy.thy	Fri Aug 18 14:57:23 2017 +0200
    25.2 +++ b/src/Doc/Typeclass_Hierarchy/Typeclass_Hierarchy.thy	Fri Aug 18 22:55:54 2017 +0200
    25.3 @@ -1,5 +1,5 @@
    25.4  theory Typeclass_Hierarchy
    25.5 -imports Setup
    25.6 +imports Typeclass_Hierarchy_Basics.Setup
    25.7  begin
    25.8  
    25.9  section \<open>Introduction\<close>
    26.1 --- a/src/HOL/Algebra/Congruence.thy	Fri Aug 18 14:57:23 2017 +0200
    26.2 +++ b/src/HOL/Algebra/Congruence.thy	Fri Aug 18 22:55:54 2017 +0200
    26.3 @@ -6,7 +6,7 @@
    26.4  theory Congruence
    26.5  imports 
    26.6    Main
    26.7 -  "~~/src/HOL/Library/FuncSet"
    26.8 +  "HOL-Library.FuncSet"
    26.9  begin
   26.10  
   26.11  section \<open>Objects\<close>
    27.1 --- a/src/HOL/Algebra/Divisibility.thy	Fri Aug 18 14:57:23 2017 +0200
    27.2 +++ b/src/HOL/Algebra/Divisibility.thy	Fri Aug 18 22:55:54 2017 +0200
    27.3 @@ -6,7 +6,7 @@
    27.4  section \<open>Divisibility in monoids and rings\<close>
    27.5  
    27.6  theory Divisibility
    27.7 -  imports "~~/src/HOL/Library/Permutation" Coset Group
    27.8 +  imports "HOL-Library.Permutation" Coset Group
    27.9  begin
   27.10  
   27.11  section \<open>Factorial Monoids\<close>
    28.1 --- a/src/HOL/Algebra/Exponent.thy	Fri Aug 18 14:57:23 2017 +0200
    28.2 +++ b/src/HOL/Algebra/Exponent.thy	Fri Aug 18 22:55:54 2017 +0200
    28.3 @@ -6,7 +6,7 @@
    28.4  *)
    28.5  
    28.6  theory Exponent
    28.7 -imports Main "~~/src/HOL/Computational_Algebra/Primes"
    28.8 +imports Main "HOL-Computational_Algebra.Primes"
    28.9  begin
   28.10  
   28.11  section \<open>Sylow's Theorem\<close>
    29.1 --- a/src/HOL/Algebra/Group.thy	Fri Aug 18 14:57:23 2017 +0200
    29.2 +++ b/src/HOL/Algebra/Group.thy	Fri Aug 18 22:55:54 2017 +0200
    29.3 @@ -5,7 +5,7 @@
    29.4  *)
    29.5  
    29.6  theory Group
    29.7 -imports Complete_Lattice "~~/src/HOL/Library/FuncSet"
    29.8 +imports Complete_Lattice "HOL-Library.FuncSet"
    29.9  begin
   29.10  
   29.11  section \<open>Monoids and Groups\<close>
    30.1 --- a/src/HOL/Algebra/IntRing.thy	Fri Aug 18 14:57:23 2017 +0200
    30.2 +++ b/src/HOL/Algebra/IntRing.thy	Fri Aug 18 22:55:54 2017 +0200
    30.3 @@ -4,7 +4,7 @@
    30.4  *)
    30.5  
    30.6  theory IntRing
    30.7 -imports "~~/src/HOL/Computational_Algebra/Primes" QuotRing Lattice Int
    30.8 +imports "HOL-Computational_Algebra.Primes" QuotRing Lattice HOL.Int
    30.9  begin
   30.10  
   30.11  section \<open>The Ring of Integers\<close>
    31.1 --- a/src/HOL/Algebra/Order.thy	Fri Aug 18 14:57:23 2017 +0200
    31.2 +++ b/src/HOL/Algebra/Order.thy	Fri Aug 18 22:55:54 2017 +0200
    31.3 @@ -8,7 +8,7 @@
    31.4  
    31.5  theory Order
    31.6  imports 
    31.7 -  "~~/src/HOL/Library/FuncSet"
    31.8 +  "HOL-Library.FuncSet"
    31.9    Congruence
   31.10  begin
   31.11  
    32.1 --- a/src/HOL/Analysis/Arcwise_Connected.thy	Fri Aug 18 14:57:23 2017 +0200
    32.2 +++ b/src/HOL/Analysis/Arcwise_Connected.thy	Fri Aug 18 22:55:54 2017 +0200
    32.3 @@ -5,7 +5,7 @@
    32.4  section \<open>Arcwise-connected sets\<close>
    32.5  
    32.6  theory Arcwise_Connected
    32.7 -  imports Path_Connected Ordered_Euclidean_Space "~~/src/HOL/Computational_Algebra/Primes"
    32.8 +  imports Path_Connected Ordered_Euclidean_Space "HOL-Computational_Algebra.Primes"
    32.9  
   32.10  begin
   32.11  
    33.1 --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Fri Aug 18 14:57:23 2017 +0200
    33.2 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Fri Aug 18 22:55:54 2017 +0200
    33.3 @@ -5,7 +5,7 @@
    33.4  section \<open>Complex Analysis Basics\<close>
    33.5  
    33.6  theory Complex_Analysis_Basics
    33.7 -imports Equivalence_Lebesgue_Henstock_Integration "~~/src/HOL/Library/Nonpos_Ints"
    33.8 +imports Equivalence_Lebesgue_Henstock_Integration "HOL-Library.Nonpos_Ints"
    33.9  begin
   33.10  
   33.11  
    34.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Fri Aug 18 14:57:23 2017 +0200
    34.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Fri Aug 18 22:55:54 2017 +0200
    34.3 @@ -6,7 +6,7 @@
    34.4  imports
    34.5    Complex_Analysis_Basics
    34.6    Summation_Tests
    34.7 -   "~~/src/HOL/Library/Periodic_Fun"
    34.8 +   "HOL-Library.Periodic_Fun"
    34.9  begin
   34.10  
   34.11  (* TODO: Figure out what to do with Möbius transformations *)
    35.1 --- a/src/HOL/Analysis/Continuum_Not_Denumerable.thy	Fri Aug 18 14:57:23 2017 +0200
    35.2 +++ b/src/HOL/Analysis/Continuum_Not_Denumerable.thy	Fri Aug 18 22:55:54 2017 +0200
    35.3 @@ -8,7 +8,7 @@
    35.4  theory Continuum_Not_Denumerable
    35.5  imports
    35.6    Complex_Main 
    35.7 -  "~~/src/HOL/Library/Countable_Set"
    35.8 +  "HOL-Library.Countable_Set"
    35.9  begin
   35.10  
   35.11  subsection \<open>Abstract\<close>
    36.1 --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Fri Aug 18 14:57:23 2017 +0200
    36.2 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Fri Aug 18 22:55:54 2017 +0200
    36.3 @@ -11,7 +11,7 @@
    36.4  theory Convex_Euclidean_Space
    36.5  imports
    36.6    Topology_Euclidean_Space
    36.7 -  "~~/src/HOL/Library/Set_Algebras"
    36.8 +  "HOL-Library.Set_Algebras"
    36.9  begin
   36.10  
   36.11  lemma swap_continuous: (*move to Topological_Spaces?*)
    37.1 --- a/src/HOL/Analysis/Determinants.thy	Fri Aug 18 14:57:23 2017 +0200
    37.2 +++ b/src/HOL/Analysis/Determinants.thy	Fri Aug 18 22:55:54 2017 +0200
    37.3 @@ -7,7 +7,7 @@
    37.4  theory Determinants
    37.5  imports
    37.6    Cartesian_Euclidean_Space
    37.7 -  "~~/src/HOL/Library/Permutations"
    37.8 +  "HOL-Library.Permutations"
    37.9  begin
   37.10  
   37.11  subsection \<open>Trace\<close>
    38.1 --- a/src/HOL/Analysis/Extended_Real_Limits.thy	Fri Aug 18 14:57:23 2017 +0200
    38.2 +++ b/src/HOL/Analysis/Extended_Real_Limits.thy	Fri Aug 18 22:55:54 2017 +0200
    38.3 @@ -10,9 +10,9 @@
    38.4  theory Extended_Real_Limits
    38.5  imports
    38.6    Topology_Euclidean_Space
    38.7 -  "~~/src/HOL/Library/Extended_Real"
    38.8 -  "~~/src/HOL/Library/Extended_Nonnegative_Real"
    38.9 -  "~~/src/HOL/Library/Indicator_Function"
   38.10 +  "HOL-Library.Extended_Real"
   38.11 +  "HOL-Library.Extended_Nonnegative_Real"
   38.12 +  "HOL-Library.Indicator_Function"
   38.13  begin
   38.14  
   38.15  lemma compact_UNIV:
    39.1 --- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Fri Aug 18 14:57:23 2017 +0200
    39.2 +++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Fri Aug 18 22:55:54 2017 +0200
    39.3 @@ -8,9 +8,9 @@
    39.4  imports
    39.5    Euclidean_Space
    39.6    L2_Norm
    39.7 -  "~~/src/HOL/Library/Numeral_Type"
    39.8 -  "~~/src/HOL/Library/Countable_Set"
    39.9 -  "~~/src/HOL/Library/FuncSet"
   39.10 +  "HOL-Library.Numeral_Type"
   39.11 +  "HOL-Library.Countable_Set"
   39.12 +  "HOL-Library.FuncSet"
   39.13  begin
   39.14  
   39.15  subsection \<open>Finite Cartesian products, with indexing and lambdas.\<close>
    40.1 --- a/src/HOL/Analysis/Gamma_Function.thy	Fri Aug 18 14:57:23 2017 +0200
    40.2 +++ b/src/HOL/Analysis/Gamma_Function.thy	Fri Aug 18 22:55:54 2017 +0200
    40.3 @@ -9,8 +9,8 @@
    40.4    Conformal_Mappings
    40.5    Summation_Tests
    40.6    Harmonic_Numbers
    40.7 -  "~~/src/HOL/Library/Nonpos_Ints"
    40.8 -  "~~/src/HOL/Library/Periodic_Fun"
    40.9 +  "HOL-Library.Nonpos_Ints"
   40.10 +  "HOL-Library.Periodic_Fun"
   40.11  begin
   40.12  
   40.13  text \<open>
    41.1 --- a/src/HOL/Analysis/L2_Norm.thy	Fri Aug 18 14:57:23 2017 +0200
    41.2 +++ b/src/HOL/Analysis/L2_Norm.thy	Fri Aug 18 22:55:54 2017 +0200
    41.3 @@ -5,7 +5,7 @@
    41.4  section \<open>Square root of sum of squares\<close>
    41.5  
    41.6  theory L2_Norm
    41.7 -imports NthRoot
    41.8 +imports HOL.NthRoot
    41.9  begin
   41.10  
   41.11  definition
    42.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Fri Aug 18 14:57:23 2017 +0200
    42.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Fri Aug 18 22:55:54 2017 +0200
    42.3 @@ -7,7 +7,7 @@
    42.4  theory Linear_Algebra
    42.5  imports
    42.6    Euclidean_Space
    42.7 -  "~~/src/HOL/Library/Infinite_Set"
    42.8 +  "HOL-Library.Infinite_Set"
    42.9  begin
   42.10  
   42.11  lemma linear_simps:
    43.1 --- a/src/HOL/Analysis/Measurable.thy	Fri Aug 18 14:57:23 2017 +0200
    43.2 +++ b/src/HOL/Analysis/Measurable.thy	Fri Aug 18 22:55:54 2017 +0200
    43.3 @@ -4,7 +4,7 @@
    43.4  theory Measurable
    43.5    imports
    43.6      Sigma_Algebra
    43.7 -    "~~/src/HOL/Library/Order_Continuity"
    43.8 +    "HOL-Library.Order_Continuity"
    43.9  begin
   43.10  
   43.11  subsection \<open>Measurability prover\<close>
    44.1 --- a/src/HOL/Analysis/Measure_Space.thy	Fri Aug 18 14:57:23 2017 +0200
    44.2 +++ b/src/HOL/Analysis/Measure_Space.thy	Fri Aug 18 22:55:54 2017 +0200
    44.3 @@ -8,7 +8,7 @@
    44.4  
    44.5  theory Measure_Space
    44.6  imports
    44.7 -  Measurable "~~/src/HOL/Library/Extended_Nonnegative_Real"
    44.8 +  Measurable "HOL-Library.Extended_Nonnegative_Real"
    44.9  begin
   44.10  
   44.11  subsection "Relate extended reals and the indicator function"
    45.1 --- a/src/HOL/Analysis/Norm_Arith.thy	Fri Aug 18 14:57:23 2017 +0200
    45.2 +++ b/src/HOL/Analysis/Norm_Arith.thy	Fri Aug 18 22:55:54 2017 +0200
    45.3 @@ -5,7 +5,7 @@
    45.4  section \<open>General linear decision procedure for normed spaces\<close>
    45.5  
    45.6  theory Norm_Arith
    45.7 -imports "~~/src/HOL/Library/Sum_of_Squares"
    45.8 +imports "HOL-Library.Sum_of_Squares"
    45.9  begin
   45.10  
   45.11  (* FIXME: move elsewhere *)
    46.1 --- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Fri Aug 18 14:57:23 2017 +0200
    46.2 +++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Fri Aug 18 22:55:54 2017 +0200
    46.3 @@ -1,7 +1,7 @@
    46.4  theory Ordered_Euclidean_Space
    46.5  imports
    46.6    Cartesian_Euclidean_Space
    46.7 -  "~~/src/HOL/Library/Product_Order"
    46.8 +  "HOL-Library.Product_Order"
    46.9  begin
   46.10  
   46.11  subsection \<open>An ordering on euclidean spaces that will allow us to talk about intervals\<close>
    47.1 --- a/src/HOL/Analysis/Product_Vector.thy	Fri Aug 18 14:57:23 2017 +0200
    47.2 +++ b/src/HOL/Analysis/Product_Vector.thy	Fri Aug 18 22:55:54 2017 +0200
    47.3 @@ -7,7 +7,7 @@
    47.4  theory Product_Vector
    47.5  imports
    47.6    Inner_Product
    47.7 -  "~~/src/HOL/Library/Product_Plus"
    47.8 +  "HOL-Library.Product_Plus"
    47.9  begin
   47.10  
   47.11  subsection \<open>Product is a real vector space\<close>
    48.1 --- a/src/HOL/Analysis/Sigma_Algebra.thy	Fri Aug 18 14:57:23 2017 +0200
    48.2 +++ b/src/HOL/Analysis/Sigma_Algebra.thy	Fri Aug 18 22:55:54 2017 +0200
    48.3 @@ -10,11 +10,11 @@
    48.4  theory Sigma_Algebra
    48.5  imports
    48.6    Complex_Main
    48.7 -  "~~/src/HOL/Library/Countable_Set"
    48.8 -  "~~/src/HOL/Library/FuncSet"
    48.9 -  "~~/src/HOL/Library/Indicator_Function"
   48.10 -  "~~/src/HOL/Library/Extended_Nonnegative_Real"
   48.11 -  "~~/src/HOL/Library/Disjoint_Sets"
   48.12 +  "HOL-Library.Countable_Set"
   48.13 +  "HOL-Library.FuncSet"
   48.14 +  "HOL-Library.Indicator_Function"
   48.15 +  "HOL-Library.Extended_Nonnegative_Real"
   48.16 +  "HOL-Library.Disjoint_Sets"
   48.17  begin
   48.18  
   48.19  text \<open>Sigma algebras are an elementary concept in measure
    49.1 --- a/src/HOL/Analysis/Summation_Tests.thy	Fri Aug 18 14:57:23 2017 +0200
    49.2 +++ b/src/HOL/Analysis/Summation_Tests.thy	Fri Aug 18 22:55:54 2017 +0200
    49.3 @@ -7,9 +7,9 @@
    49.4  theory Summation_Tests
    49.5  imports
    49.6    Complex_Main
    49.7 -  "~~/src/HOL/Library/Discrete"
    49.8 -  "~~/src/HOL/Library/Extended_Real"
    49.9 -  "~~/src/HOL/Library/Liminf_Limsup"
   49.10 +  "HOL-Library.Discrete"
   49.11 +  "HOL-Library.Extended_Real"
   49.12 +  "HOL-Library.Liminf_Limsup"
   49.13  begin
   49.14  
   49.15  text \<open>
    50.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Fri Aug 18 14:57:23 2017 +0200
    50.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Fri Aug 18 22:55:54 2017 +0200
    50.3 @@ -8,9 +8,9 @@
    50.4  
    50.5  theory Topology_Euclidean_Space
    50.6  imports
    50.7 -  "~~/src/HOL/Library/Indicator_Function"
    50.8 -  "~~/src/HOL/Library/Countable_Set"
    50.9 -  "~~/src/HOL/Library/FuncSet"
   50.10 +  "HOL-Library.Indicator_Function"
   50.11 +  "HOL-Library.Countable_Set"
   50.12 +  "HOL-Library.FuncSet"
   50.13    Linear_Algebra
   50.14    Norm_Arith
   50.15  begin
    51.1 --- a/src/HOL/Analysis/ex/Approximations.thy	Fri Aug 18 14:57:23 2017 +0200
    51.2 +++ b/src/HOL/Analysis/ex/Approximations.thy	Fri Aug 18 22:55:54 2017 +0200
    51.3 @@ -1,7 +1,7 @@
    51.4  section \<open>Numeric approximations to Constants\<close>
    51.5  
    51.6  theory Approximations
    51.7 -imports "../Complex_Transcendental" "../Harmonic_Numbers"
    51.8 +imports "HOL-Analysis.Complex_Transcendental" "HOL-Analysis.Harmonic_Numbers"
    51.9  begin
   51.10  
   51.11  text \<open>
    52.1 --- a/src/HOL/Analysis/ex/Circle_Area.thy	Fri Aug 18 14:57:23 2017 +0200
    52.2 +++ b/src/HOL/Analysis/ex/Circle_Area.thy	Fri Aug 18 22:55:54 2017 +0200
    52.3 @@ -7,7 +7,7 @@
    52.4  section \<open>The area of a circle\<close>
    52.5  
    52.6  theory Circle_Area
    52.7 -imports Complex_Main Interval_Integral
    52.8 +imports Complex_Main "HOL-Analysis.Interval_Integral"
    52.9  begin
   52.10  
   52.11  lemma plus_emeasure':
    53.1 --- a/src/HOL/Auth/Smartcard/EventSC.thy	Fri Aug 18 14:57:23 2017 +0200
    53.2 +++ b/src/HOL/Auth/Smartcard/EventSC.thy	Fri Aug 18 22:55:54 2017 +0200
    53.3 @@ -3,7 +3,7 @@
    53.4  theory EventSC
    53.5  imports
    53.6    "../Message"
    53.7 -  "~~/src/HOL/Library/Simps_Case_Conv"
    53.8 +  "HOL-Library.Simps_Case_Conv"
    53.9  begin
   53.10  
   53.11  consts  (*Initial states of agents -- parameter of the construction*)
    54.1 --- a/src/HOL/Auth/TLS.thy	Fri Aug 18 14:57:23 2017 +0200
    54.2 +++ b/src/HOL/Auth/TLS.thy	Fri Aug 18 22:55:54 2017 +0200
    54.3 @@ -40,7 +40,7 @@
    54.4  
    54.5  section\<open>The TLS Protocol: Transport Layer Security\<close>
    54.6  
    54.7 -theory TLS imports Public "~~/src/HOL/Library/Nat_Bijection" begin
    54.8 +theory TLS imports Public "HOL-Library.Nat_Bijection" begin
    54.9  
   54.10  definition certificate :: "[agent,key] => msg" where
   54.11      "certificate A KA == Crypt (priSK Server) \<lbrace>Agent A, Key KA\<rbrace>"
    55.1 --- a/src/HOL/Bali/Basis.thy	Fri Aug 18 14:57:23 2017 +0200
    55.2 +++ b/src/HOL/Bali/Basis.thy	Fri Aug 18 22:55:54 2017 +0200
    55.3 @@ -4,7 +4,7 @@
    55.4  subsection \<open>Definitions extending HOL as logical basis of Bali\<close>
    55.5  
    55.6  theory Basis
    55.7 -imports Main "~~/src/HOL/Library/Old_Recdef"
    55.8 +imports Main "HOL-Library.Old_Recdef"
    55.9  begin
   55.10  
   55.11  subsubsection "misc"
    56.1 --- a/src/HOL/Cardinals/Cardinal_Arithmetic.thy	Fri Aug 18 14:57:23 2017 +0200
    56.2 +++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy	Fri Aug 18 22:55:54 2017 +0200
    56.3 @@ -8,7 +8,7 @@
    56.4  section \<open>Cardinal Arithmetic\<close>
    56.5  
    56.6  theory Cardinal_Arithmetic
    56.7 -imports BNF_Cardinal_Arithmetic Cardinal_Order_Relation
    56.8 +imports HOL.BNF_Cardinal_Arithmetic Cardinal_Order_Relation
    56.9  begin
   56.10  
   56.11  subsection \<open>Binary sum\<close>
    57.1 --- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Fri Aug 18 14:57:23 2017 +0200
    57.2 +++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Fri Aug 18 22:55:54 2017 +0200
    57.3 @@ -8,7 +8,7 @@
    57.4  section \<open>Cardinal-Order Relations\<close>
    57.5  
    57.6  theory Cardinal_Order_Relation
    57.7 -imports BNF_Cardinal_Order_Relation Wellorder_Constructions
    57.8 +imports HOL.BNF_Cardinal_Order_Relation Wellorder_Constructions
    57.9  begin
   57.10  
   57.11  declare
    58.1 --- a/src/HOL/Cardinals/Order_Union.thy	Fri Aug 18 14:57:23 2017 +0200
    58.2 +++ b/src/HOL/Cardinals/Order_Union.thy	Fri Aug 18 22:55:54 2017 +0200
    58.3 @@ -7,7 +7,7 @@
    58.4  section \<open>Order Union\<close>
    58.5  
    58.6  theory Order_Union
    58.7 -imports Order_Relation
    58.8 +imports HOL.Order_Relation
    58.9  begin
   58.10  
   58.11  definition Osum :: "'a rel \<Rightarrow> 'a rel \<Rightarrow> 'a rel"  (infix "Osum" 60) where
    59.1 --- a/src/HOL/Cardinals/Wellfounded_More.thy	Fri Aug 18 14:57:23 2017 +0200
    59.2 +++ b/src/HOL/Cardinals/Wellfounded_More.thy	Fri Aug 18 22:55:54 2017 +0200
    59.3 @@ -8,7 +8,7 @@
    59.4  section \<open>More on Well-Founded Relations\<close>
    59.5  
    59.6  theory Wellfounded_More
    59.7 -imports Wellfounded Order_Relation_More
    59.8 +imports HOL.Wellfounded Order_Relation_More
    59.9  begin
   59.10  
   59.11  subsection \<open>Well-founded recursion via genuine fixpoints\<close>
    60.1 --- a/src/HOL/Cardinals/Wellorder_Constructions.thy	Fri Aug 18 14:57:23 2017 +0200
    60.2 +++ b/src/HOL/Cardinals/Wellorder_Constructions.thy	Fri Aug 18 22:55:54 2017 +0200
    60.3 @@ -9,8 +9,8 @@
    60.4  
    60.5  theory Wellorder_Constructions
    60.6  imports
    60.7 -  BNF_Wellorder_Constructions Wellorder_Embedding Order_Union
    60.8 -  "../Library/Cardinal_Notations"
    60.9 +  HOL.BNF_Wellorder_Constructions Wellorder_Embedding Order_Union
   60.10 +  "HOL-Library.Cardinal_Notations"
   60.11  begin
   60.12  
   60.13  declare
    61.1 --- a/src/HOL/Cardinals/Wellorder_Embedding.thy	Fri Aug 18 14:57:23 2017 +0200
    61.2 +++ b/src/HOL/Cardinals/Wellorder_Embedding.thy	Fri Aug 18 22:55:54 2017 +0200
    61.3 @@ -8,7 +8,7 @@
    61.4  section \<open>Well-Order Embeddings\<close>
    61.5  
    61.6  theory Wellorder_Embedding
    61.7 -imports BNF_Wellorder_Embedding Fun_More Wellorder_Relation
    61.8 +imports HOL.BNF_Wellorder_Embedding Fun_More Wellorder_Relation
    61.9  begin
   61.10  
   61.11  subsection \<open>Auxiliaries\<close>
    62.1 --- a/src/HOL/Cardinals/Wellorder_Relation.thy	Fri Aug 18 14:57:23 2017 +0200
    62.2 +++ b/src/HOL/Cardinals/Wellorder_Relation.thy	Fri Aug 18 22:55:54 2017 +0200
    62.3 @@ -8,7 +8,7 @@
    62.4  section \<open>Well-Order Relations\<close>
    62.5  
    62.6  theory Wellorder_Relation
    62.7 -imports BNF_Wellorder_Relation Wellfounded_More
    62.8 +imports HOL.BNF_Wellorder_Relation Wellfounded_More
    62.9  begin
   62.10  
   62.11  context wo_rel
    63.1 --- a/src/HOL/Codegenerator_Test/Candidates.thy	Fri Aug 18 14:57:23 2017 +0200
    63.2 +++ b/src/HOL/Codegenerator_Test/Candidates.thy	Fri Aug 18 22:55:54 2017 +0200
    63.3 @@ -6,15 +6,15 @@
    63.4  theory Candidates
    63.5  imports
    63.6    Complex_Main
    63.7 -  "~~/src/HOL/Library/Library"
    63.8 -  "~~/src/HOL/Library/Subseq_Order"
    63.9 -  "~~/src/HOL/Library/RBT"
   63.10 -  "~~/src/HOL/Data_Structures/Tree_Map"
   63.11 -  "~~/src/HOL/Data_Structures/Tree_Set"
   63.12 -  "~~/src/HOL/Computational_Algebra/Computational_Algebra"
   63.13 -  "~~/src/HOL/Computational_Algebra/Polynomial_Factorial"
   63.14 -  "~~/src/HOL/Number_Theory/Eratosthenes"
   63.15 -  "~~/src/HOL/ex/Records"
   63.16 +  "HOL-Library.Library"
   63.17 +  "HOL-Library.Subseq_Order"
   63.18 +  "HOL-Library.RBT"
   63.19 +  "HOL-Data_Structures.Tree_Map"
   63.20 +  "HOL-Data_Structures.Tree_Set"
   63.21 +  "HOL-Computational_Algebra.Computational_Algebra"
   63.22 +  "HOL-Computational_Algebra.Polynomial_Factorial"
   63.23 +  "HOL-Number_Theory.Eratosthenes"
   63.24 +  "HOL-ex.Records"
   63.25  begin
   63.26  
   63.27  text \<open>Drop technical stuff from @{theory Quickcheck_Narrowing} which is tailored towards Haskell\<close>
    64.1 --- a/src/HOL/Codegenerator_Test/Code_Test_GHC.thy	Fri Aug 18 14:57:23 2017 +0200
    64.2 +++ b/src/HOL/Codegenerator_Test/Code_Test_GHC.thy	Fri Aug 18 22:55:54 2017 +0200
    64.3 @@ -4,7 +4,7 @@
    64.4  Test case for test_code on GHC
    64.5  *)
    64.6  
    64.7 -theory Code_Test_GHC imports "../Library/Code_Test" begin
    64.8 +theory Code_Test_GHC imports "HOL-Library.Code_Test" begin
    64.9  
   64.10  test_code "(14 + 7 * -12 :: integer) = 140 div -2" in GHC
   64.11  
    65.1 --- a/src/HOL/Codegenerator_Test/Code_Test_MLton.thy	Fri Aug 18 14:57:23 2017 +0200
    65.2 +++ b/src/HOL/Codegenerator_Test/Code_Test_MLton.thy	Fri Aug 18 22:55:54 2017 +0200
    65.3 @@ -4,7 +4,7 @@
    65.4  Test case for test_code on MLton
    65.5  *)
    65.6  
    65.7 -theory Code_Test_MLton imports  "../Library/Code_Test" begin
    65.8 +theory Code_Test_MLton imports  "HOL-Library.Code_Test" begin
    65.9  
   65.10  test_code "14 + 7 * -12 = (140 div -2 :: integer)" in MLton
   65.11  
    66.1 --- a/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy	Fri Aug 18 14:57:23 2017 +0200
    66.2 +++ b/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy	Fri Aug 18 22:55:54 2017 +0200
    66.3 @@ -4,7 +4,7 @@
    66.4  Test case for test_code on OCaml
    66.5  *)
    66.6  
    66.7 -theory Code_Test_OCaml imports  "../Library/Code_Test" begin
    66.8 +theory Code_Test_OCaml imports  "HOL-Library.Code_Test" begin
    66.9  
   66.10  test_code "14 + 7 * -12 = (140 div -2 :: integer)" in OCaml
   66.11  
    67.1 --- a/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy	Fri Aug 18 14:57:23 2017 +0200
    67.2 +++ b/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy	Fri Aug 18 22:55:54 2017 +0200
    67.3 @@ -4,7 +4,7 @@
    67.4  Test case for test_code on PolyML
    67.5  *)
    67.6  
    67.7 -theory Code_Test_PolyML imports  "../Library/Code_Test" begin
    67.8 +theory Code_Test_PolyML imports  "HOL-Library.Code_Test" begin
    67.9  
   67.10  test_code "14 + 7 * -12 = (140 div -2 :: integer)" in PolyML
   67.11  
    68.1 --- a/src/HOL/Codegenerator_Test/Code_Test_SMLNJ.thy	Fri Aug 18 14:57:23 2017 +0200
    68.2 +++ b/src/HOL/Codegenerator_Test/Code_Test_SMLNJ.thy	Fri Aug 18 22:55:54 2017 +0200
    68.3 @@ -4,7 +4,7 @@
    68.4  Test case for test_code on SMLNJ
    68.5  *)
    68.6  
    68.7 -theory Code_Test_SMLNJ imports  "../Library/Code_Test" begin
    68.8 +theory Code_Test_SMLNJ imports  "HOL-Library.Code_Test" begin
    68.9  
   68.10  test_code "14 + 7 * -12 = (140 div -2 :: integer)" in SMLNJ
   68.11  
    69.1 --- a/src/HOL/Codegenerator_Test/Code_Test_Scala.thy	Fri Aug 18 14:57:23 2017 +0200
    69.2 +++ b/src/HOL/Codegenerator_Test/Code_Test_Scala.thy	Fri Aug 18 22:55:54 2017 +0200
    69.3 @@ -4,7 +4,7 @@
    69.4  Test case for test_code on Scala
    69.5  *)
    69.6  
    69.7 -theory Code_Test_Scala imports  "../Library/Code_Test" begin
    69.8 +theory Code_Test_Scala imports  "HOL-Library.Code_Test" begin
    69.9  
   69.10  declare [[scala_case_insensitive]]
   69.11  
    70.1 --- a/src/HOL/Codegenerator_Test/Generate.thy	Fri Aug 18 14:57:23 2017 +0200
    70.2 +++ b/src/HOL/Codegenerator_Test/Generate.thy	Fri Aug 18 22:55:54 2017 +0200
    70.3 @@ -6,8 +6,8 @@
    70.4  theory Generate
    70.5  imports
    70.6    Candidates
    70.7 -  "~~/src/HOL/Library/AList_Mapping"
    70.8 -  "~~/src/HOL/Library/Finite_Lattice"
    70.9 +  "HOL-Library.AList_Mapping"
   70.10 +  "HOL-Library.Finite_Lattice"
   70.11  begin
   70.12  
   70.13  text \<open>
    71.1 --- a/src/HOL/Codegenerator_Test/Generate_Binary_Nat.thy	Fri Aug 18 14:57:23 2017 +0200
    71.2 +++ b/src/HOL/Codegenerator_Test/Generate_Binary_Nat.thy	Fri Aug 18 22:55:54 2017 +0200
    71.3 @@ -6,9 +6,9 @@
    71.4  theory Generate_Binary_Nat
    71.5  imports
    71.6    Candidates
    71.7 -  "~~/src/HOL/Library/AList_Mapping"
    71.8 -  "~~/src/HOL/Library/Finite_Lattice"
    71.9 -  "~~/src/HOL/Library/Code_Binary_Nat"
   71.10 +  "HOL-Library.AList_Mapping"
   71.11 +  "HOL-Library.Finite_Lattice"
   71.12 +  "HOL-Library.Code_Binary_Nat"
   71.13  begin
   71.14  
   71.15  text \<open>
    72.1 --- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Fri Aug 18 14:57:23 2017 +0200
    72.2 +++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Fri Aug 18 22:55:54 2017 +0200
    72.3 @@ -6,9 +6,9 @@
    72.4  theory Generate_Efficient_Datastructures
    72.5  imports
    72.6    Candidates
    72.7 -  "~~/src/HOL/Library/DAList_Multiset"
    72.8 -  "~~/src/HOL/Library/RBT_Mapping"
    72.9 -  "~~/src/HOL/Library/RBT_Set"
   72.10 +  "HOL-Library.DAList_Multiset"
   72.11 +  "HOL-Library.RBT_Mapping"
   72.12 +  "HOL-Library.RBT_Set"
   72.13  begin
   72.14  
   72.15  text \<open>
    73.1 --- a/src/HOL/Codegenerator_Test/Generate_Pretty_Char.thy	Fri Aug 18 14:57:23 2017 +0200
    73.2 +++ b/src/HOL/Codegenerator_Test/Generate_Pretty_Char.thy	Fri Aug 18 22:55:54 2017 +0200
    73.3 @@ -6,9 +6,9 @@
    73.4  theory Generate_Pretty_Char
    73.5  imports
    73.6    Candidates
    73.7 -  "~~/src/HOL/Library/AList_Mapping"
    73.8 -  "~~/src/HOL/Library/Finite_Lattice"
    73.9 -  "~~/src/HOL/Library/Code_Char"
   73.10 +  "HOL-Library.AList_Mapping"
   73.11 +  "HOL-Library.Finite_Lattice"
   73.12 +  "HOL-Library.Code_Char"
   73.13  begin
   73.14  
   73.15  text \<open>
    74.1 --- a/src/HOL/Codegenerator_Test/Generate_Target_Nat.thy	Fri Aug 18 14:57:23 2017 +0200
    74.2 +++ b/src/HOL/Codegenerator_Test/Generate_Target_Nat.thy	Fri Aug 18 22:55:54 2017 +0200
    74.3 @@ -6,9 +6,9 @@
    74.4  theory Generate_Target_Nat
    74.5  imports
    74.6    Candidates
    74.7 -  "~~/src/HOL/Library/AList_Mapping"
    74.8 -  "~~/src/HOL/Library/Finite_Lattice"
    74.9 -  "~~/src/HOL/Library/Code_Target_Numeral"
   74.10 +  "HOL-Library.AList_Mapping"
   74.11 +  "HOL-Library.Finite_Lattice"
   74.12 +  "HOL-Library.Code_Target_Numeral"
   74.13  begin
   74.14  
   74.15  text \<open>
    75.1 --- a/src/HOL/Computational_Algebra/Factorial_Ring.thy	Fri Aug 18 14:57:23 2017 +0200
    75.2 +++ b/src/HOL/Computational_Algebra/Factorial_Ring.thy	Fri Aug 18 22:55:54 2017 +0200
    75.3 @@ -8,7 +8,7 @@
    75.4  theory Factorial_Ring
    75.5  imports
    75.6    Main
    75.7 -  "~~/src/HOL/Library/Multiset"
    75.8 +  "HOL-Library.Multiset"
    75.9  begin
   75.10  
   75.11  subsection \<open>Irreducible and prime elements\<close>
    76.1 --- a/src/HOL/Computational_Algebra/Polynomial.thy	Fri Aug 18 14:57:23 2017 +0200
    76.2 +++ b/src/HOL/Computational_Algebra/Polynomial.thy	Fri Aug 18 22:55:54 2017 +0200
    76.3 @@ -9,9 +9,9 @@
    76.4  
    76.5  theory Polynomial
    76.6  imports
    76.7 -  "~~/src/HOL/Deriv"
    76.8 -  "~~/src/HOL/Library/More_List"
    76.9 -  "~~/src/HOL/Library/Infinite_Set"
   76.10 +  HOL.Deriv
   76.11 +  "HOL-Library.More_List"
   76.12 +  "HOL-Library.Infinite_Set"
   76.13  begin
   76.14  
   76.15  subsection \<open>Auxiliary: operations for lists (later) representing coefficients\<close>
    77.1 --- a/src/HOL/Computational_Algebra/Primes.thy	Fri Aug 18 14:57:23 2017 +0200
    77.2 +++ b/src/HOL/Computational_Algebra/Primes.thy	Fri Aug 18 22:55:54 2017 +0200
    77.3 @@ -39,7 +39,7 @@
    77.4  section \<open>Primes\<close>
    77.5  
    77.6  theory Primes
    77.7 -imports "~~/src/HOL/Binomial" Euclidean_Algorithm
    77.8 +imports HOL.Binomial Euclidean_Algorithm
    77.9  begin
   77.10  
   77.11  (* As a simp or intro rule,
    78.1 --- a/src/HOL/Corec_Examples/LFilter.thy	Fri Aug 18 14:57:23 2017 +0200
    78.2 +++ b/src/HOL/Corec_Examples/LFilter.thy	Fri Aug 18 22:55:54 2017 +0200
    78.3 @@ -10,7 +10,7 @@
    78.4  section \<open>The Filter Function on Lazy Lists\<close>
    78.5  
    78.6  theory LFilter
    78.7 -imports "~~/src/HOL/Library/BNF_Corec"
    78.8 +imports "HOL-Library.BNF_Corec"
    78.9  begin
   78.10  
   78.11  codatatype (lset: 'a) llist =
    79.1 --- a/src/HOL/Corec_Examples/Paper_Examples.thy	Fri Aug 18 14:57:23 2017 +0200
    79.2 +++ b/src/HOL/Corec_Examples/Paper_Examples.thy	Fri Aug 18 22:55:54 2017 +0200
    79.3 @@ -9,7 +9,7 @@
    79.4  section \<open>Small Examples from the Paper ``Friends with Benefits''\<close>
    79.5  
    79.6  theory Paper_Examples
    79.7 -imports "~~/src/HOL/Library/BNF_Corec" "~~/src/HOL/Library/FSet" Complex_Main
    79.8 +imports "HOL-Library.BNF_Corec" "HOL-Library.FSet" Complex_Main
    79.9  begin
   79.10  
   79.11  section \<open>Examples from the introduction\<close>
    80.1 --- a/src/HOL/Corec_Examples/Stream_Processor.thy	Fri Aug 18 14:57:23 2017 +0200
    80.2 +++ b/src/HOL/Corec_Examples/Stream_Processor.thy	Fri Aug 18 22:55:54 2017 +0200
    80.3 @@ -10,7 +10,7 @@
    80.4  section \<open>Stream Processors---A Syntactic Representation of Continuous Functions on Streams\<close>
    80.5  
    80.6  theory Stream_Processor
    80.7 -imports "~~/src/HOL/Library/BNF_Corec" "~~/src/HOL/Library/Stream"
    80.8 +imports "HOL-Library.BNF_Corec" "HOL-Library.Stream"
    80.9  begin
   80.10  
   80.11  datatype (discs_sels) ('a, 'b, 'c) sp\<^sub>\<mu> =
    81.1 --- a/src/HOL/Corec_Examples/Tests/GPV_Bare_Bones.thy	Fri Aug 18 14:57:23 2017 +0200
    81.2 +++ b/src/HOL/Corec_Examples/Tests/GPV_Bare_Bones.thy	Fri Aug 18 22:55:54 2017 +0200
    81.3 @@ -9,7 +9,7 @@
    81.4  section \<open>A Bare Bones Version of Generative Probabilistic Values (GPVs)\<close>
    81.5  
    81.6  theory GPV_Bare_Bones
    81.7 -imports "~~/src/HOL/Library/BNF_Corec"
    81.8 +imports "HOL-Library.BNF_Corec"
    81.9  begin
   81.10  
   81.11  datatype 'a pmf = return_pmf 'a
    82.1 --- a/src/HOL/Corec_Examples/Tests/Iterate_GPV.thy	Fri Aug 18 14:57:23 2017 +0200
    82.2 +++ b/src/HOL/Corec_Examples/Tests/Iterate_GPV.thy	Fri Aug 18 22:55:54 2017 +0200
    82.3 @@ -1,6 +1,6 @@
    82.4  theory Iterate_GPV imports
    82.5 -  "~~/src/HOL/Library/BNF_Axiomatization"
    82.6 -  "~~/src/HOL/Library/BNF_Corec"
    82.7 +  "HOL-Library.BNF_Axiomatization"
    82.8 +  "HOL-Library.BNF_Corec"
    82.9  begin
   82.10  
   82.11  declare [[typedef_overloaded]]
    83.1 --- a/src/HOL/Corec_Examples/Tests/Merge_A.thy	Fri Aug 18 14:57:23 2017 +0200
    83.2 +++ b/src/HOL/Corec_Examples/Tests/Merge_A.thy	Fri Aug 18 22:55:54 2017 +0200
    83.3 @@ -9,7 +9,7 @@
    83.4  section \<open>Tests Theory Merges\<close>
    83.5  
    83.6  theory Merge_A
    83.7 -imports "~~/src/HOL/Library/BNF_Corec"
    83.8 +imports "HOL-Library.BNF_Corec"
    83.9  begin
   83.10  
   83.11  codatatype 'a ta = Ca (sa1: 'a) (sa2: "'a ta")
    84.1 --- a/src/HOL/Corec_Examples/Tests/Merge_Poly.thy	Fri Aug 18 14:57:23 2017 +0200
    84.2 +++ b/src/HOL/Corec_Examples/Tests/Merge_Poly.thy	Fri Aug 18 22:55:54 2017 +0200
    84.3 @@ -9,7 +9,7 @@
    84.4  section \<open>Tests Polymorphic Merges\<close>
    84.5  
    84.6  theory Merge_Poly
    84.7 -imports "~~/src/HOL/Library/BNF_Corec"
    84.8 +imports "HOL-Library.BNF_Corec"
    84.9  begin
   84.10  
   84.11  subsection \<open>A Monomorphic Example\<close>
    85.1 --- a/src/HOL/Corec_Examples/Tests/Misc_Mono.thy	Fri Aug 18 14:57:23 2017 +0200
    85.2 +++ b/src/HOL/Corec_Examples/Tests/Misc_Mono.thy	Fri Aug 18 22:55:54 2017 +0200
    85.3 @@ -9,7 +9,7 @@
    85.4  section \<open>Miscellaneous Monomorphic Examples\<close>
    85.5  
    85.6  theory Misc_Mono
    85.7 -imports "~~/src/HOL/Library/BNF_Corec"
    85.8 +imports "HOL-Library.BNF_Corec"
    85.9  begin
   85.10  
   85.11  codatatype T0 =
    86.1 --- a/src/HOL/Corec_Examples/Tests/Misc_Poly.thy	Fri Aug 18 14:57:23 2017 +0200
    86.2 +++ b/src/HOL/Corec_Examples/Tests/Misc_Poly.thy	Fri Aug 18 22:55:54 2017 +0200
    86.3 @@ -9,7 +9,7 @@
    86.4  section \<open>Miscellaneous Polymorphic Examples\<close>
    86.5  
    86.6  theory Misc_Poly
    86.7 -imports "~~/src/HOL/Library/BNF_Corec"
    86.8 +imports "HOL-Library.BNF_Corec"
    86.9  begin
   86.10  
   86.11  codatatype ('a, 'b) T0 =
    87.1 --- a/src/HOL/Corec_Examples/Tests/Simple_Nesting.thy	Fri Aug 18 14:57:23 2017 +0200
    87.2 +++ b/src/HOL/Corec_Examples/Tests/Simple_Nesting.thy	Fri Aug 18 22:55:54 2017 +0200
    87.3 @@ -9,7 +9,7 @@
    87.4  section \<open>Tests "corec"'s Parsing of Map Functions\<close>
    87.5  
    87.6  theory Simple_Nesting
    87.7 -imports "~~/src/HOL/Library/BNF_Corec"
    87.8 +imports "HOL-Library.BNF_Corec"
    87.9  begin
   87.10  
   87.11  subsection \<open>Corecursion via Map Functions\<close>
    88.1 --- a/src/HOL/Corec_Examples/Tests/Small_Concrete.thy	Fri Aug 18 14:57:23 2017 +0200
    88.2 +++ b/src/HOL/Corec_Examples/Tests/Small_Concrete.thy	Fri Aug 18 22:55:54 2017 +0200
    88.3 @@ -9,7 +9,7 @@
    88.4  section \<open>Small Concrete Examples\<close>
    88.5  
    88.6  theory Small_Concrete
    88.7 -imports "~~/src/HOL/Library/BNF_Corec"
    88.8 +imports "HOL-Library.BNF_Corec"
    88.9  begin
   88.10  
   88.11  subsection \<open>Streams of Natural Numbers\<close>
    89.1 --- a/src/HOL/Corec_Examples/Tests/Stream_Friends.thy	Fri Aug 18 14:57:23 2017 +0200
    89.2 +++ b/src/HOL/Corec_Examples/Tests/Stream_Friends.thy	Fri Aug 18 22:55:54 2017 +0200
    89.3 @@ -9,7 +9,7 @@
    89.4  section \<open>Friendly Functions on Streams\<close>
    89.5  
    89.6  theory Stream_Friends
    89.7 -imports "~~/src/HOL/Library/BNF_Corec"
    89.8 +imports "HOL-Library.BNF_Corec"
    89.9  begin
   89.10  
   89.11  codatatype 'a stream = SCons (shd: 'a) (stl: "'a stream")
    90.1 --- a/src/HOL/Corec_Examples/Tests/TLList_Friends.thy	Fri Aug 18 14:57:23 2017 +0200
    90.2 +++ b/src/HOL/Corec_Examples/Tests/TLList_Friends.thy	Fri Aug 18 22:55:54 2017 +0200
    90.3 @@ -9,7 +9,7 @@
    90.4  section \<open>Friendly Functions on Terminated Lists\<close>
    90.5  
    90.6  theory TLList_Friends
    90.7 -imports "~~/src/HOL/Library/BNF_Corec"
    90.8 +imports "HOL-Library.BNF_Corec"
    90.9  begin
   90.10  
   90.11  codatatype ('a, 'b) tllist =
    91.1 --- a/src/HOL/Corec_Examples/Tests/Type_Class.thy	Fri Aug 18 14:57:23 2017 +0200
    91.2 +++ b/src/HOL/Corec_Examples/Tests/Type_Class.thy	Fri Aug 18 22:55:54 2017 +0200
    91.3 @@ -9,7 +9,7 @@
    91.4  section \<open>Tests Type Class Instances as Friends\<close>
    91.5  
    91.6  theory Type_Class
    91.7 -imports "~~/src/HOL/Library/BNF_Corec" "~~/src/HOL/Library/Stream"
    91.8 +imports "HOL-Library.BNF_Corec" "HOL-Library.Stream"
    91.9  begin
   91.10  
   91.11  instantiation stream :: (plus) plus
    92.1 --- a/src/HOL/Data_Structures/AVL_Set.thy	Fri Aug 18 14:57:23 2017 +0200
    92.2 +++ b/src/HOL/Data_Structures/AVL_Set.thy	Fri Aug 18 22:55:54 2017 +0200
    92.3 @@ -9,7 +9,7 @@
    92.4  imports
    92.5   Cmp
    92.6   Isin2
    92.7 -  "~~/src/HOL/Number_Theory/Fib"
    92.8 +  "HOL-Number_Theory.Fib"
    92.9  begin
   92.10  
   92.11  type_synonym 'a avl_tree = "('a,nat) tree"
    93.1 --- a/src/HOL/Data_Structures/Balance.thy	Fri Aug 18 14:57:23 2017 +0200
    93.2 +++ b/src/HOL/Data_Structures/Balance.thy	Fri Aug 18 22:55:54 2017 +0200
    93.3 @@ -5,7 +5,7 @@
    93.4  theory Balance
    93.5  imports
    93.6    Complex_Main
    93.7 -  "~~/src/HOL/Library/Tree"
    93.8 +  "HOL-Library.Tree"
    93.9  begin
   93.10  
   93.11  (* The following two lemmas should go into theory \<open>Tree\<close>, except that that
    94.1 --- a/src/HOL/Data_Structures/Brother12_Set.thy	Fri Aug 18 14:57:23 2017 +0200
    94.2 +++ b/src/HOL/Data_Structures/Brother12_Set.thy	Fri Aug 18 22:55:54 2017 +0200
    94.3 @@ -6,7 +6,7 @@
    94.4  imports
    94.5    Cmp
    94.6    Set_by_Ordered
    94.7 -  "~~/src/HOL/Number_Theory/Fib"
    94.8 +  "HOL-Number_Theory.Fib"
    94.9  begin
   94.10  
   94.11  subsection \<open>Data Type and Operations\<close>
    95.1 --- a/src/HOL/Data_Structures/Priority_Queue.thy	Fri Aug 18 14:57:23 2017 +0200
    95.2 +++ b/src/HOL/Data_Structures/Priority_Queue.thy	Fri Aug 18 22:55:54 2017 +0200
    95.3 @@ -3,7 +3,7 @@
    95.4  section \<open>Priority Queue Interface\<close>
    95.5  
    95.6  theory Priority_Queue
    95.7 -imports "~~/src/HOL/Library/Multiset"
    95.8 +imports "HOL-Library.Multiset"
    95.9  begin
   95.10  
   95.11  text \<open>Priority queue interface:\<close>
    96.1 --- a/src/HOL/Data_Structures/Splay_Set.thy	Fri Aug 18 14:57:23 2017 +0200
    96.2 +++ b/src/HOL/Data_Structures/Splay_Set.thy	Fri Aug 18 22:55:54 2017 +0200
    96.3 @@ -7,7 +7,7 @@
    96.4  
    96.5  theory Splay_Set
    96.6  imports
    96.7 -  "~~/src/HOL/Library/Tree"
    96.8 +  "HOL-Library.Tree"
    96.9    Set_by_Ordered
   96.10    Cmp
   96.11  begin
    97.1 --- a/src/HOL/Data_Structures/Tree_Set.thy	Fri Aug 18 14:57:23 2017 +0200
    97.2 +++ b/src/HOL/Data_Structures/Tree_Set.thy	Fri Aug 18 22:55:54 2017 +0200
    97.3 @@ -4,7 +4,7 @@
    97.4  
    97.5  theory Tree_Set
    97.6  imports
    97.7 -  "~~/src/HOL/Library/Tree"
    97.8 +  "HOL-Library.Tree"
    97.9    Cmp
   97.10    Set_by_Ordered
   97.11  begin
    98.1 --- a/src/HOL/Datatype_Examples/Compat.thy	Fri Aug 18 14:57:23 2017 +0200
    98.2 +++ b/src/HOL/Datatype_Examples/Compat.thy	Fri Aug 18 22:55:54 2017 +0200
    98.3 @@ -8,7 +8,7 @@
    98.4  section \<open>Tests for Compatibility with the Old Datatype Package\<close>
    98.5  
    98.6  theory Compat
    98.7 -imports "~~/src/HOL/Library/Old_Datatype"
    98.8 +imports "HOL-Library.Old_Datatype"
    98.9  begin
   98.10  
   98.11  subsection \<open>Viewing and Registering New-Style Datatypes as Old-Style Ones\<close>
    99.1 --- a/src/HOL/Datatype_Examples/Derivation_Trees/Gram_Lang.thy	Fri Aug 18 14:57:23 2017 +0200
    99.2 +++ b/src/HOL/Datatype_Examples/Derivation_Trees/Gram_Lang.thy	Fri Aug 18 22:55:54 2017 +0200
    99.3 @@ -8,7 +8,7 @@
    99.4  section \<open>Language of a Grammar\<close>
    99.5  
    99.6  theory Gram_Lang
    99.7 -imports DTree "~~/src/HOL/Library/Infinite_Set"
    99.8 +imports DTree "HOL-Library.Infinite_Set"
    99.9  begin
   99.10  
   99.11  
   100.1 --- a/src/HOL/Datatype_Examples/Derivation_Trees/Prelim.thy	Fri Aug 18 14:57:23 2017 +0200
   100.2 +++ b/src/HOL/Datatype_Examples/Derivation_Trees/Prelim.thy	Fri Aug 18 22:55:54 2017 +0200
   100.3 @@ -8,7 +8,7 @@
   100.4  section \<open>Preliminaries\<close>
   100.5  
   100.6  theory Prelim
   100.7 -imports "~~/src/HOL/Library/FSet"
   100.8 +imports "HOL-Library.FSet"
   100.9  begin
  100.10  
  100.11  notation BNF_Def.convol ("\<langle>(_,/ _)\<rangle>")
   101.1 --- a/src/HOL/Datatype_Examples/Koenig.thy	Fri Aug 18 14:57:23 2017 +0200
   101.2 +++ b/src/HOL/Datatype_Examples/Koenig.thy	Fri Aug 18 22:55:54 2017 +0200
   101.3 @@ -9,7 +9,7 @@
   101.4  section \<open>Koenig's Lemma\<close>
   101.5  
   101.6  theory Koenig
   101.7 -imports TreeFI "~~/src/HOL/Library/Stream"
   101.8 +imports TreeFI "HOL-Library.Stream"
   101.9  begin
  101.10  
  101.11  (* infinite trees: *)
   102.1 --- a/src/HOL/Datatype_Examples/Lambda_Term.thy	Fri Aug 18 14:57:23 2017 +0200
   102.2 +++ b/src/HOL/Datatype_Examples/Lambda_Term.thy	Fri Aug 18 22:55:54 2017 +0200
   102.3 @@ -9,7 +9,7 @@
   102.4  section \<open>Lambda-Terms\<close>
   102.5  
   102.6  theory Lambda_Term
   102.7 -imports "~~/src/HOL/Library/FSet"
   102.8 +imports "HOL-Library.FSet"
   102.9  begin
  102.10  
  102.11  section \<open>Datatype definition\<close>
   103.1 --- a/src/HOL/Datatype_Examples/Misc_Codatatype.thy	Fri Aug 18 14:57:23 2017 +0200
   103.2 +++ b/src/HOL/Datatype_Examples/Misc_Codatatype.thy	Fri Aug 18 22:55:54 2017 +0200
   103.3 @@ -10,7 +10,7 @@
   103.4  section \<open>Miscellaneous Codatatype Definitions\<close>
   103.5  
   103.6  theory Misc_Codatatype
   103.7 -imports "~~/src/HOL/Library/FSet"
   103.8 +imports "HOL-Library.FSet"
   103.9  begin
  103.10  
  103.11  codatatype simple = X1 | X2 | X3 | X4
   104.1 --- a/src/HOL/Datatype_Examples/Misc_Datatype.thy	Fri Aug 18 14:57:23 2017 +0200
   104.2 +++ b/src/HOL/Datatype_Examples/Misc_Datatype.thy	Fri Aug 18 22:55:54 2017 +0200
   104.3 @@ -10,7 +10,7 @@
   104.4  section \<open>Miscellaneous Datatype Definitions\<close>
   104.5  
   104.6  theory Misc_Datatype
   104.7 -imports "~~/src/HOL/Library/Countable" "~~/src/HOL/Library/FSet"
   104.8 +imports "HOL-Library.Countable" "HOL-Library.FSet"
   104.9  begin
  104.10  
  104.11  datatype (discs_sels) simple = X1 | X2 | X3 | X4
   105.1 --- a/src/HOL/Datatype_Examples/Process.thy	Fri Aug 18 14:57:23 2017 +0200
   105.2 +++ b/src/HOL/Datatype_Examples/Process.thy	Fri Aug 18 22:55:54 2017 +0200
   105.3 @@ -8,7 +8,7 @@
   105.4  section \<open>Processes\<close>
   105.5  
   105.6  theory Process
   105.7 -imports "~~/src/HOL/Library/Stream"
   105.8 +imports "HOL-Library.Stream"
   105.9  begin
  105.10  
  105.11  codatatype 'a process =
   106.1 --- a/src/HOL/Datatype_Examples/Stream_Processor.thy	Fri Aug 18 14:57:23 2017 +0200
   106.2 +++ b/src/HOL/Datatype_Examples/Stream_Processor.thy	Fri Aug 18 22:55:54 2017 +0200
   106.3 @@ -9,7 +9,7 @@
   106.4  section \<open>Stream Processors---A Syntactic Representation of Continuous Functions on Streams\<close>
   106.5  
   106.6  theory Stream_Processor
   106.7 -imports "~~/src/HOL/Library/Stream" "~~/src/HOL/Library/BNF_Axiomatization"
   106.8 +imports "HOL-Library.Stream" "HOL-Library.BNF_Axiomatization"
   106.9  begin
  106.10  
  106.11  declare [[typedef_overloaded]]
   107.1 --- a/src/HOL/Datatype_Examples/TreeFsetI.thy	Fri Aug 18 14:57:23 2017 +0200
   107.2 +++ b/src/HOL/Datatype_Examples/TreeFsetI.thy	Fri Aug 18 22:55:54 2017 +0200
   107.3 @@ -9,7 +9,7 @@
   107.4  section \<open>Finitely Branching Possibly Infinite Trees, with Sets of Children\<close>
   107.5  
   107.6  theory TreeFsetI
   107.7 -imports "~~/src/HOL/Library/FSet"
   107.8 +imports "HOL-Library.FSet"
   107.9  begin
  107.10  
  107.11  codatatype 'a treeFsetI = Tree (lab: 'a) (sub: "'a treeFsetI fset")
   108.1 --- a/src/HOL/Decision_Procs/Algebra_Aux.thy	Fri Aug 18 14:57:23 2017 +0200
   108.2 +++ b/src/HOL/Decision_Procs/Algebra_Aux.thy	Fri Aug 18 22:55:54 2017 +0200
   108.3 @@ -5,7 +5,7 @@
   108.4  section \<open>Things that can be added to the Algebra library\<close>
   108.5  
   108.6  theory Algebra_Aux
   108.7 -imports "~~/src/HOL/Algebra/Ring"
   108.8 +imports "HOL-Algebra.Ring"
   108.9  begin
  108.10  
  108.11  definition of_natural :: "('a, 'm) ring_scheme \<Rightarrow> nat \<Rightarrow> 'a" ("\<guillemotleft>_\<guillemotright>\<^sub>\<nat>\<index>") where
   109.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Fri Aug 18 14:57:23 2017 +0200
   109.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Fri Aug 18 22:55:54 2017 +0200
   109.3 @@ -4,7 +4,7 @@
   109.4  theory Approximation
   109.5  imports
   109.6    Complex_Main
   109.7 -  "~~/src/HOL/Library/Code_Target_Numeral"
   109.8 +  "HOL-Library.Code_Target_Numeral"
   109.9    Approximation_Bounds
  109.10  keywords "approximate" :: diag
  109.11  begin
   110.1 --- a/src/HOL/Decision_Procs/Approximation_Bounds.thy	Fri Aug 18 14:57:23 2017 +0200
   110.2 +++ b/src/HOL/Decision_Procs/Approximation_Bounds.thy	Fri Aug 18 22:55:54 2017 +0200
   110.3 @@ -11,7 +11,7 @@
   110.4  theory Approximation_Bounds
   110.5  imports
   110.6    Complex_Main
   110.7 -  "~~/src/HOL/Library/Float"
   110.8 +  "HOL-Library.Float"
   110.9    Dense_Linear_Order
  110.10  begin
  110.11  
   111.1 --- a/src/HOL/Decision_Procs/Commutative_Ring.thy	Fri Aug 18 14:57:23 2017 +0200
   111.2 +++ b/src/HOL/Decision_Procs/Commutative_Ring.thy	Fri Aug 18 22:55:54 2017 +0200
   111.3 @@ -10,7 +10,7 @@
   111.4  imports
   111.5    Conversions
   111.6    Algebra_Aux
   111.7 -  "~~/src/HOL/Library/Code_Target_Numeral"
   111.8 +  "HOL-Library.Code_Target_Numeral"
   111.9  begin
  111.10  
  111.11  text \<open>Syntax of multivariate polynomials (pol) and polynomial expressions.\<close>
   112.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Fri Aug 18 14:57:23 2017 +0200
   112.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Fri Aug 18 22:55:54 2017 +0200
   112.3 @@ -5,8 +5,8 @@
   112.4  theory Cooper
   112.5  imports
   112.6    Complex_Main
   112.7 -  "~~/src/HOL/Library/Code_Target_Numeral"
   112.8 -  "~~/src/HOL/Library/Old_Recdef"
   112.9 +  "HOL-Library.Code_Target_Numeral"
  112.10 +  "HOL-Library.Old_Recdef"
  112.11  begin
  112.12  
  112.13  (* Periodicity of dvd *)
   113.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Fri Aug 18 14:57:23 2017 +0200
   113.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Fri Aug 18 22:55:54 2017 +0200
   113.3 @@ -4,7 +4,7 @@
   113.4  
   113.5  theory Ferrack
   113.6  imports Complex_Main Dense_Linear_Order DP_Library
   113.7 -  "~~/src/HOL/Library/Code_Target_Numeral" "~~/src/HOL/Library/Old_Recdef"
   113.8 +  "HOL-Library.Code_Target_Numeral" "HOL-Library.Old_Recdef"
   113.9  begin
  113.10  
  113.11  section \<open>Quantifier elimination for \<open>\<real> (0, 1, +, <)\<close>\<close>
   114.1 --- a/src/HOL/Decision_Procs/MIR.thy	Fri Aug 18 14:57:23 2017 +0200
   114.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Fri Aug 18 22:55:54 2017 +0200
   114.3 @@ -4,7 +4,7 @@
   114.4  
   114.5  theory MIR
   114.6  imports Complex_Main Dense_Linear_Order DP_Library
   114.7 -  "~~/src/HOL/Library/Code_Target_Numeral" "~~/src/HOL/Library/Old_Recdef"
   114.8 +  "HOL-Library.Code_Target_Numeral" "HOL-Library.Old_Recdef"
   114.9  begin
  114.10  
  114.11  section \<open>Quantifier elimination for \<open>\<real> (0, 1, +, floor, <)\<close>\<close>
   115.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Aug 18 14:57:23 2017 +0200
   115.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Aug 18 22:55:54 2017 +0200
   115.3 @@ -9,8 +9,8 @@
   115.4    Reflected_Multivariate_Polynomial
   115.5    Dense_Linear_Order
   115.6    DP_Library
   115.7 -  "~~/src/HOL/Library/Code_Target_Numeral"
   115.8 -  "~~/src/HOL/Library/Old_Recdef"
   115.9 +  "HOL-Library.Code_Target_Numeral"
  115.10 +  "HOL-Library.Old_Recdef"
  115.11  begin
  115.12  
  115.13  subsection \<open>Terms\<close>
   116.1 --- a/src/HOL/Eisbach/Examples_FOL.thy	Fri Aug 18 14:57:23 2017 +0200
   116.2 +++ b/src/HOL/Eisbach/Examples_FOL.thy	Fri Aug 18 22:55:54 2017 +0200
   116.3 @@ -5,7 +5,7 @@
   116.4  section \<open>Basic Eisbach examples (in FOL)\<close>
   116.5  
   116.6  theory Examples_FOL
   116.7 -imports "~~/src/FOL/FOL" Eisbach_Old_Appl_Syntax
   116.8 +imports FOL Eisbach_Old_Appl_Syntax
   116.9  begin
  116.10  
  116.11  
   117.1 --- a/src/HOL/HOLCF/Bifinite.thy	Fri Aug 18 14:57:23 2017 +0200
   117.2 +++ b/src/HOL/HOLCF/Bifinite.thy	Fri Aug 18 22:55:54 2017 +0200
   117.3 @@ -5,7 +5,7 @@
   117.4  section \<open>Profinite and bifinite cpos\<close>
   117.5  
   117.6  theory Bifinite
   117.7 -imports Map_Functions Cprod Sprod Sfun Up "~~/src/HOL/Library/Countable"
   117.8 +imports Map_Functions Cprod Sprod Sfun Up "HOL-Library.Countable"
   117.9  begin
  117.10  
  117.11  default_sort cpo
   118.1 --- a/src/HOL/HOLCF/FOCUS/Fstream.thy	Fri Aug 18 14:57:23 2017 +0200
   118.2 +++ b/src/HOL/HOLCF/FOCUS/Fstream.thy	Fri Aug 18 22:55:54 2017 +0200
   118.3 @@ -9,7 +9,7 @@
   118.4  section \<open>FOCUS flat streams\<close>
   118.5  
   118.6  theory Fstream
   118.7 -imports "~~/src/HOL/HOLCF/Library/Stream"
   118.8 +imports "HOLCF-Library.Stream"
   118.9  begin
  118.10  
  118.11  default_sort type
   119.1 --- a/src/HOL/HOLCF/FOCUS/Fstreams.thy	Fri Aug 18 14:57:23 2017 +0200
   119.2 +++ b/src/HOL/HOLCF/FOCUS/Fstreams.thy	Fri Aug 18 22:55:54 2017 +0200
   119.3 @@ -7,7 +7,7 @@
   119.4  *)
   119.5  
   119.6  theory Fstreams
   119.7 -imports "~~/src/HOL/HOLCF/Library/Stream"
   119.8 +imports "HOLCF-Library.Stream"
   119.9  begin
  119.10  
  119.11  default_sort type
   120.1 --- a/src/HOL/HOLCF/FOCUS/Stream_adm.thy	Fri Aug 18 14:57:23 2017 +0200
   120.2 +++ b/src/HOL/HOLCF/FOCUS/Stream_adm.thy	Fri Aug 18 22:55:54 2017 +0200
   120.3 @@ -5,7 +5,7 @@
   120.4  section \<open>Admissibility for streams\<close>
   120.5  
   120.6  theory Stream_adm
   120.7 -imports "~~/src/HOL/HOLCF/Library/Stream" "~~/src/HOL/Library/Order_Continuity"
   120.8 +imports "HOLCF-Library.Stream" "HOL-Library.Order_Continuity"
   120.9  begin
  120.10  
  120.11  definition
   121.1 --- a/src/HOL/HOLCF/IMP/Denotational.thy	Fri Aug 18 14:57:23 2017 +0200
   121.2 +++ b/src/HOL/HOLCF/IMP/Denotational.thy	Fri Aug 18 22:55:54 2017 +0200
   121.3 @@ -5,7 +5,7 @@
   121.4  
   121.5  section "Denotational Semantics of Commands in HOLCF"
   121.6  
   121.7 -theory Denotational imports HOLCF "~~/src/HOL/IMP/Big_Step" begin
   121.8 +theory Denotational imports HOLCF "HOL-IMP.Big_Step" begin
   121.9  
  121.10  subsection "Definition"
  121.11  
   122.1 --- a/src/HOL/HOLCF/IOA/ABP/Abschannel.thy	Fri Aug 18 14:57:23 2017 +0200
   122.2 +++ b/src/HOL/HOLCF/IOA/ABP/Abschannel.thy	Fri Aug 18 22:55:54 2017 +0200
   122.3 @@ -5,7 +5,7 @@
   122.4  section \<open>The transmission channel\<close>
   122.5  
   122.6  theory Abschannel
   122.7 -imports "../IOA" Action Lemmas
   122.8 +imports IOA.IOA Action Lemmas
   122.9  begin
  122.10  
  122.11  datatype 'a abs_action = S 'a | R 'a
   123.1 --- a/src/HOL/HOLCF/IOA/ABP/Abschannel_finite.thy	Fri Aug 18 14:57:23 2017 +0200
   123.2 +++ b/src/HOL/HOLCF/IOA/ABP/Abschannel_finite.thy	Fri Aug 18 22:55:54 2017 +0200
   123.3 @@ -5,7 +5,7 @@
   123.4  section \<open>The transmission channel -- finite version\<close>
   123.5  
   123.6  theory Abschannel_finite
   123.7 -imports Abschannel "../IOA" Action Lemmas
   123.8 +imports Abschannel IOA.IOA Action Lemmas
   123.9  begin
  123.10  
  123.11  primrec reverse :: "'a list => 'a list"
   124.1 --- a/src/HOL/HOLCF/IOA/ABP/Correctness.thy	Fri Aug 18 14:57:23 2017 +0200
   124.2 +++ b/src/HOL/HOLCF/IOA/ABP/Correctness.thy	Fri Aug 18 22:55:54 2017 +0200
   124.3 @@ -5,7 +5,7 @@
   124.4  section \<open>The main correctness proof: System_fin implements System\<close>
   124.5  
   124.6  theory Correctness
   124.7 -imports "../IOA" Env Impl Impl_finite
   124.8 +imports IOA.IOA Env Impl Impl_finite
   124.9  begin
  124.10  
  124.11  ML_file "Check.ML"
   125.1 --- a/src/HOL/HOLCF/IOA/ABP/Env.thy	Fri Aug 18 14:57:23 2017 +0200
   125.2 +++ b/src/HOL/HOLCF/IOA/ABP/Env.thy	Fri Aug 18 22:55:54 2017 +0200
   125.3 @@ -5,7 +5,7 @@
   125.4  section \<open>The environment\<close>
   125.5  
   125.6  theory Env
   125.7 -imports "../IOA" Action
   125.8 +imports IOA.IOA Action
   125.9  begin
  125.10  
  125.11  type_synonym
   126.1 --- a/src/HOL/HOLCF/IOA/ABP/Receiver.thy	Fri Aug 18 14:57:23 2017 +0200
   126.2 +++ b/src/HOL/HOLCF/IOA/ABP/Receiver.thy	Fri Aug 18 22:55:54 2017 +0200
   126.3 @@ -5,7 +5,7 @@
   126.4  section \<open>The implementation: receiver\<close>
   126.5  
   126.6  theory Receiver
   126.7 -imports "../IOA" Action Lemmas
   126.8 +imports IOA.IOA Action Lemmas
   126.9  begin
  126.10  
  126.11  type_synonym
   127.1 --- a/src/HOL/HOLCF/IOA/ABP/Sender.thy	Fri Aug 18 14:57:23 2017 +0200
   127.2 +++ b/src/HOL/HOLCF/IOA/ABP/Sender.thy	Fri Aug 18 22:55:54 2017 +0200
   127.3 @@ -5,7 +5,7 @@
   127.4  section \<open>The implementation: sender\<close>
   127.5  
   127.6  theory Sender
   127.7 -imports "../IOA" Action Lemmas
   127.8 +imports IOA.IOA Action Lemmas
   127.9  begin
  127.10  
  127.11  type_synonym
   128.1 --- a/src/HOL/HOLCF/IOA/ABP/Spec.thy	Fri Aug 18 14:57:23 2017 +0200
   128.2 +++ b/src/HOL/HOLCF/IOA/ABP/Spec.thy	Fri Aug 18 22:55:54 2017 +0200
   128.3 @@ -5,7 +5,7 @@
   128.4  section \<open>The specification of reliable transmission\<close>
   128.5  
   128.6  theory Spec
   128.7 -imports "../IOA" Action
   128.8 +imports IOA.IOA Action
   128.9  begin
  128.10  
  128.11  definition
   129.1 --- a/src/HOL/HOLCF/IOA/NTP/Abschannel.thy	Fri Aug 18 14:57:23 2017 +0200
   129.2 +++ b/src/HOL/HOLCF/IOA/NTP/Abschannel.thy	Fri Aug 18 22:55:54 2017 +0200
   129.3 @@ -5,7 +5,7 @@
   129.4  section \<open>The (faulty) transmission channel (both directions)\<close>
   129.5  
   129.6  theory Abschannel
   129.7 -imports "../IOA" Action
   129.8 +imports IOA.IOA Action
   129.9  begin
  129.10  
  129.11  datatype 'a abs_action = S 'a | R 'a
   130.1 --- a/src/HOL/HOLCF/IOA/NTP/Receiver.thy	Fri Aug 18 14:57:23 2017 +0200
   130.2 +++ b/src/HOL/HOLCF/IOA/NTP/Receiver.thy	Fri Aug 18 22:55:54 2017 +0200
   130.3 @@ -5,7 +5,7 @@
   130.4  section \<open>The implementation: receiver\<close>
   130.5  
   130.6  theory Receiver
   130.7 -imports "../IOA" Action
   130.8 +imports IOA.IOA Action
   130.9  begin
  130.10  
  130.11  type_synonym
   131.1 --- a/src/HOL/HOLCF/IOA/NTP/Sender.thy	Fri Aug 18 14:57:23 2017 +0200
   131.2 +++ b/src/HOL/HOLCF/IOA/NTP/Sender.thy	Fri Aug 18 22:55:54 2017 +0200
   131.3 @@ -5,7 +5,7 @@
   131.4  section \<open>The implementation: sender\<close>
   131.5  
   131.6  theory Sender
   131.7 -imports "../IOA" Action
   131.8 +imports IOA.IOA Action
   131.9  begin
  131.10  
  131.11  type_synonym
   132.1 --- a/src/HOL/HOLCF/IOA/NTP/Spec.thy	Fri Aug 18 14:57:23 2017 +0200
   132.2 +++ b/src/HOL/HOLCF/IOA/NTP/Spec.thy	Fri Aug 18 22:55:54 2017 +0200
   132.3 @@ -5,7 +5,7 @@
   132.4  section \<open>The specification of reliable transmission\<close>
   132.5  
   132.6  theory Spec
   132.7 -imports "../IOA" Action
   132.8 +imports IOA.IOA Action
   132.9  begin
  132.10  
  132.11  definition
   133.1 --- a/src/HOL/HOLCF/IOA/Seq.thy	Fri Aug 18 14:57:23 2017 +0200
   133.2 +++ b/src/HOL/HOLCF/IOA/Seq.thy	Fri Aug 18 22:55:54 2017 +0200
   133.3 @@ -5,7 +5,7 @@
   133.4  section \<open>Partial, Finite and Infinite Sequences (lazy lists), modeled as domain\<close>
   133.5  
   133.6  theory Seq
   133.7 -imports "../HOLCF"
   133.8 +imports HOLCF
   133.9  begin
  133.10  
  133.11  default_sort pcpo
   134.1 --- a/src/HOL/HOLCF/IOA/Storage/Correctness.thy	Fri Aug 18 14:57:23 2017 +0200
   134.2 +++ b/src/HOL/HOLCF/IOA/Storage/Correctness.thy	Fri Aug 18 22:55:54 2017 +0200
   134.3 @@ -5,7 +5,7 @@
   134.4  section \<open>Correctness Proof\<close>
   134.5  
   134.6  theory Correctness
   134.7 -imports "../SimCorrectness" Spec Impl
   134.8 +imports IOA.SimCorrectness Spec Impl
   134.9  begin
  134.10  
  134.11  default_sort type
   135.1 --- a/src/HOL/HOLCF/IOA/Storage/Impl.thy	Fri Aug 18 14:57:23 2017 +0200
   135.2 +++ b/src/HOL/HOLCF/IOA/Storage/Impl.thy	Fri Aug 18 22:55:54 2017 +0200
   135.3 @@ -5,7 +5,7 @@
   135.4  section \<open>The implementation of a memory\<close>
   135.5  
   135.6  theory Impl
   135.7 -imports "../IOA" Action
   135.8 +imports IOA.IOA Action
   135.9  begin
  135.10  
  135.11  definition
   136.1 --- a/src/HOL/HOLCF/IOA/Storage/Spec.thy	Fri Aug 18 14:57:23 2017 +0200
   136.2 +++ b/src/HOL/HOLCF/IOA/Storage/Spec.thy	Fri Aug 18 22:55:54 2017 +0200
   136.3 @@ -5,7 +5,7 @@
   136.4  section \<open>The specification of a memory\<close>
   136.5  
   136.6  theory Spec
   136.7 -imports "../IOA" Action
   136.8 +imports IOA.IOA Action
   136.9  begin
  136.10  
  136.11  definition
   137.1 --- a/src/HOL/HOLCF/IOA/ex/TrivEx.thy	Fri Aug 18 14:57:23 2017 +0200
   137.2 +++ b/src/HOL/HOLCF/IOA/ex/TrivEx.thy	Fri Aug 18 22:55:54 2017 +0200
   137.3 @@ -5,7 +5,7 @@
   137.4  section \<open>Trivial Abstraction Example\<close>
   137.5  
   137.6  theory TrivEx
   137.7 -imports "../Abstraction"
   137.8 +imports IOA.Abstraction
   137.9  begin
  137.10  
  137.11  datatype action = INC
   138.1 --- a/src/HOL/HOLCF/IOA/ex/TrivEx2.thy	Fri Aug 18 14:57:23 2017 +0200
   138.2 +++ b/src/HOL/HOLCF/IOA/ex/TrivEx2.thy	Fri Aug 18 22:55:54 2017 +0200
   138.3 @@ -5,7 +5,7 @@
   138.4  section \<open>Trivial Abstraction Example with fairness\<close>
   138.5  
   138.6  theory TrivEx2
   138.7 -imports "../Abstraction"
   138.8 +imports IOA.Abstraction
   138.9  begin
  138.10  
  138.11  datatype action = INC
   139.1 --- a/src/HOL/HOLCF/Library/Defl_Bifinite.thy	Fri Aug 18 14:57:23 2017 +0200
   139.2 +++ b/src/HOL/HOLCF/Library/Defl_Bifinite.thy	Fri Aug 18 22:55:54 2017 +0200
   139.3 @@ -5,7 +5,7 @@
   139.4  section \<open>Algebraic deflations are a bifinite domain\<close>
   139.5  
   139.6  theory Defl_Bifinite
   139.7 -imports HOLCF "~~/src/HOL/Library/Infinite_Set"
   139.8 +imports HOLCF "HOL-Library.Infinite_Set"
   139.9  begin
  139.10  
  139.11  subsection \<open>Lemmas about MOST\<close>
   140.1 --- a/src/HOL/HOLCF/Library/Stream.thy	Fri Aug 18 14:57:23 2017 +0200
   140.2 +++ b/src/HOL/HOLCF/Library/Stream.thy	Fri Aug 18 22:55:54 2017 +0200
   140.3 @@ -5,7 +5,7 @@
   140.4  section \<open>General Stream domain\<close>
   140.5  
   140.6  theory Stream
   140.7 -imports "../HOLCF" "~~/src/HOL/Library/Extended_Nat"
   140.8 +imports HOLCF "HOL-Library.Extended_Nat"
   140.9  begin
  140.10  
  140.11  default_sort pcpo
   141.1 --- a/src/HOL/HOLCF/Representable.thy	Fri Aug 18 14:57:23 2017 +0200
   141.2 +++ b/src/HOL/HOLCF/Representable.thy	Fri Aug 18 22:55:54 2017 +0200
   141.3 @@ -5,7 +5,7 @@
   141.4  section \<open>Representable domains\<close>
   141.5  
   141.6  theory Representable
   141.7 -imports Algebraic Map_Functions "~~/src/HOL/Library/Countable"
   141.8 +imports Algebraic Map_Functions "HOL-Library.Countable"
   141.9  begin
  141.10  
  141.11  default_sort cpo
   142.1 --- a/src/HOL/HOLCF/Universal.thy	Fri Aug 18 14:57:23 2017 +0200
   142.2 +++ b/src/HOL/HOLCF/Universal.thy	Fri Aug 18 22:55:54 2017 +0200
   142.3 @@ -5,7 +5,7 @@
   142.4  section \<open>A universal bifinite domain\<close>
   142.5  
   142.6  theory Universal
   142.7 -imports Bifinite Completion "~~/src/HOL/Library/Nat_Bijection"
   142.8 +imports Bifinite Completion "HOL-Library.Nat_Bijection"
   142.9  begin
  142.10  
  142.11  no_notation binomial  (infixl "choose" 65)
   143.1 --- a/src/HOL/HOLCF/ex/Dagstuhl.thy	Fri Aug 18 14:57:23 2017 +0200
   143.2 +++ b/src/HOL/HOLCF/ex/Dagstuhl.thy	Fri Aug 18 22:55:54 2017 +0200
   143.3 @@ -1,5 +1,5 @@
   143.4  theory Dagstuhl
   143.5 -imports "~~/src/HOL/HOLCF/Library/Stream"
   143.6 +imports "HOLCF-Library.Stream"
   143.7  begin
   143.8  
   143.9  axiomatization
   144.1 --- a/src/HOL/HOLCF/ex/Focus_ex.thy	Fri Aug 18 14:57:23 2017 +0200
   144.2 +++ b/src/HOL/HOLCF/ex/Focus_ex.thy	Fri Aug 18 22:55:54 2017 +0200
   144.3 @@ -99,7 +99,7 @@
   144.4  *)
   144.5  
   144.6  theory Focus_ex
   144.7 -imports "~~/src/HOL/HOLCF/Library/Stream"
   144.8 +imports "HOLCF-Library.Stream"
   144.9  begin
  144.10  
  144.11  typedecl ('a, 'b) tc
   145.1 --- a/src/HOL/Hahn_Banach/Bounds.thy	Fri Aug 18 14:57:23 2017 +0200
   145.2 +++ b/src/HOL/Hahn_Banach/Bounds.thy	Fri Aug 18 22:55:54 2017 +0200
   145.3 @@ -5,7 +5,7 @@
   145.4  section \<open>Bounds\<close>
   145.5  
   145.6  theory Bounds
   145.7 -imports Main "~~/src/HOL/Analysis/Continuum_Not_Denumerable"
   145.8 +imports Main "HOL-Analysis.Continuum_Not_Denumerable"
   145.9  begin
  145.10  
  145.11  locale lub =
   146.1 --- a/src/HOL/Hahn_Banach/Subspace.thy	Fri Aug 18 14:57:23 2017 +0200
   146.2 +++ b/src/HOL/Hahn_Banach/Subspace.thy	Fri Aug 18 22:55:54 2017 +0200
   146.3 @@ -5,7 +5,7 @@
   146.4  section \<open>Subspaces\<close>
   146.5  
   146.6  theory Subspace
   146.7 -imports Vector_Space "~~/src/HOL/Library/Set_Algebras"
   146.8 +imports Vector_Space "HOL-Library.Set_Algebras"
   146.9  begin
  146.10  
  146.11  subsection \<open>Definition\<close>
   147.1 --- a/src/HOL/IMP/Abs_Int_init.thy	Fri Aug 18 14:57:23 2017 +0200
   147.2 +++ b/src/HOL/IMP/Abs_Int_init.thy	Fri Aug 18 22:55:54 2017 +0200
   147.3 @@ -1,6 +1,6 @@
   147.4  theory Abs_Int_init
   147.5 -imports "~~/src/HOL/Library/While_Combinator"
   147.6 -        "~~/src/HOL/Library/Extended"
   147.7 +imports "HOL-Library.While_Combinator"
   147.8 +        "HOL-Library.Extended"
   147.9          Vars Collecting Abs_Int_Tests
  147.10  begin
  147.11  
   148.1 --- a/src/HOL/IMP/Live_True.thy	Fri Aug 18 14:57:23 2017 +0200
   148.2 +++ b/src/HOL/IMP/Live_True.thy	Fri Aug 18 22:55:54 2017 +0200
   148.3 @@ -1,7 +1,7 @@
   148.4  (* Author: Tobias Nipkow *)
   148.5  
   148.6  theory Live_True
   148.7 -imports "~~/src/HOL/Library/While_Combinator" Vars Big_Step
   148.8 +imports "HOL-Library.While_Combinator" Vars Big_Step
   148.9  begin
  148.10  
  148.11  subsection "True Liveness Analysis"
   149.1 --- a/src/HOL/Imperative_HOL/Heap.thy	Fri Aug 18 14:57:23 2017 +0200
   149.2 +++ b/src/HOL/Imperative_HOL/Heap.thy	Fri Aug 18 22:55:54 2017 +0200
   149.3 @@ -5,7 +5,7 @@
   149.4  section \<open>A polymorphic heap based on cantor encodings\<close>
   149.5  
   149.6  theory Heap
   149.7 -imports Main "~~/src/HOL/Library/Countable"
   149.8 +imports Main "HOL-Library.Countable"
   149.9  begin
  149.10  
  149.11  subsection \<open>Representable types\<close>
   150.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Aug 18 14:57:23 2017 +0200
   150.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Aug 18 22:55:54 2017 +0200
   150.3 @@ -7,7 +7,7 @@
   150.4  theory Heap_Monad
   150.5  imports
   150.6    Heap
   150.7 -  "~~/src/HOL/Library/Monad_Syntax"
   150.8 +  "HOL-Library.Monad_Syntax"
   150.9  begin
  150.10  
  150.11  subsection \<open>The monad\<close>
   151.1 --- a/src/HOL/Imperative_HOL/Overview.thy	Fri Aug 18 14:57:23 2017 +0200
   151.2 +++ b/src/HOL/Imperative_HOL/Overview.thy	Fri Aug 18 22:55:54 2017 +0200
   151.3 @@ -4,7 +4,7 @@
   151.4  
   151.5  (*<*)
   151.6  theory Overview
   151.7 -imports Imperative_HOL "~~/src/HOL/Library/LaTeXsugar"
   151.8 +imports Imperative_HOL "HOL-Library.LaTeXsugar"
   151.9  begin
  151.10  
  151.11  (* type constraints with spacing *)
   152.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Fri Aug 18 14:57:23 2017 +0200
   152.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Fri Aug 18 22:55:54 2017 +0200
   152.3 @@ -8,8 +8,8 @@
   152.4  imports
   152.5    "~~/src/HOL/Imperative_HOL/Imperative_HOL"
   152.6    Subarray
   152.7 -  "~~/src/HOL/Library/Multiset"
   152.8 -  "~~/src/HOL/Library/Code_Target_Numeral"
   152.9 +  "HOL-Library.Multiset"
  152.10 +  "HOL-Library.Code_Target_Numeral"
  152.11  begin
  152.12  
  152.13  text \<open>We prove QuickSort correct in the Relational Calculus.\<close>
   153.1 --- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Fri Aug 18 14:57:23 2017 +0200
   153.2 +++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Fri Aug 18 22:55:54 2017 +0200
   153.3 @@ -5,7 +5,7 @@
   153.4  section \<open>Linked Lists by ML references\<close>
   153.5  
   153.6  theory Linked_Lists
   153.7 -imports "../Imperative_HOL" "~~/src/HOL/Library/Code_Target_Int"
   153.8 +imports "../Imperative_HOL" "HOL-Library.Code_Target_Int"
   153.9  begin
  153.10  
  153.11  section \<open>Definition of Linked Lists\<close>
   154.1 --- a/src/HOL/Imperative_HOL/ex/List_Sublist.thy	Fri Aug 18 14:57:23 2017 +0200
   154.2 +++ b/src/HOL/Imperative_HOL/ex/List_Sublist.thy	Fri Aug 18 22:55:54 2017 +0200
   154.3 @@ -5,7 +5,7 @@
   154.4  section \<open>Slices of lists\<close>
   154.5  
   154.6  theory List_Sublist
   154.7 -imports "~~/src/HOL/Library/Multiset"
   154.8 +imports "HOL-Library.Multiset"
   154.9  begin
  154.10  
  154.11  lemma nths_split: "i \<le> j \<and> j \<le> k \<Longrightarrow> nths xs {i..<j} @ nths xs {j..<k} = nths xs {i..<k}" 
   155.1 --- a/src/HOL/Imperative_HOL/ex/SatChecker.thy	Fri Aug 18 14:57:23 2017 +0200
   155.2 +++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy	Fri Aug 18 22:55:54 2017 +0200
   155.3 @@ -5,7 +5,7 @@
   155.4  section \<open>An efficient checker for proofs from a SAT solver\<close>
   155.5  
   155.6  theory SatChecker
   155.7 -imports "~~/src/HOL/Library/RBT_Impl" Sorted_List "../Imperative_HOL"
   155.8 +imports "HOL-Library.RBT_Impl" Sorted_List "../Imperative_HOL"
   155.9  begin
  155.10  
  155.11  section\<open>General settings and functions for our representation of clauses\<close>
   156.1 --- a/src/HOL/Induct/Sexp.thy	Fri Aug 18 14:57:23 2017 +0200
   156.2 +++ b/src/HOL/Induct/Sexp.thy	Fri Aug 18 22:55:54 2017 +0200
   156.3 @@ -7,7 +7,7 @@
   156.4  *)
   156.5  
   156.6  theory Sexp
   156.7 -imports "~~/src/HOL/Library/Old_Datatype"
   156.8 +imports "HOL-Library.Old_Datatype"
   156.9  begin
  156.10  
  156.11  type_synonym 'a item = "'a Old_Datatype.item"
   157.1 --- a/src/HOL/Isar_Examples/Fibonacci.thy	Fri Aug 18 14:57:23 2017 +0200
   157.2 +++ b/src/HOL/Isar_Examples/Fibonacci.thy	Fri Aug 18 22:55:54 2017 +0200
   157.3 @@ -15,7 +15,7 @@
   157.4  section \<open>Fib and Gcd commute\<close>
   157.5  
   157.6  theory Fibonacci
   157.7 -  imports "../Computational_Algebra/Primes"
   157.8 +  imports "HOL-Computational_Algebra.Primes"
   157.9  begin
  157.10  
  157.11  text_raw \<open>\<^footnote>\<open>Isar version by Gertrud Bauer. Original tactic script by Larry
   158.1 --- a/src/HOL/Isar_Examples/Knaster_Tarski.thy	Fri Aug 18 14:57:23 2017 +0200
   158.2 +++ b/src/HOL/Isar_Examples/Knaster_Tarski.thy	Fri Aug 18 22:55:54 2017 +0200
   158.3 @@ -7,7 +7,7 @@
   158.4  section \<open>Textbook-style reasoning: the Knaster-Tarski Theorem\<close>
   158.5  
   158.6  theory Knaster_Tarski
   158.7 -  imports Main "~~/src/HOL/Library/Lattice_Syntax"
   158.8 +  imports Main "HOL-Library.Lattice_Syntax"
   158.9  begin
  158.10  
  158.11  
   159.1 --- a/src/HOL/Library/Countable.thy	Fri Aug 18 14:57:23 2017 +0200
   159.2 +++ b/src/HOL/Library/Countable.thy	Fri Aug 18 22:55:54 2017 +0200
   159.3 @@ -7,7 +7,7 @@
   159.4  section \<open>Encoding (almost) everything into natural numbers\<close>
   159.5  
   159.6  theory Countable
   159.7 -imports Old_Datatype "~~/src/HOL/Rat" Nat_Bijection
   159.8 +imports Old_Datatype HOL.Rat Nat_Bijection
   159.9  begin
  159.10  
  159.11  subsection \<open>The class of countable types\<close>
   160.1 --- a/src/HOL/Library/Countable_Set_Type.thy	Fri Aug 18 14:57:23 2017 +0200
   160.2 +++ b/src/HOL/Library/Countable_Set_Type.thy	Fri Aug 18 22:55:54 2017 +0200
   160.3 @@ -9,7 +9,7 @@
   160.4  section \<open>Type of (at Most) Countable Sets\<close>
   160.5  
   160.6  theory Countable_Set_Type
   160.7 -imports Countable_Set Cardinal_Notations Conditionally_Complete_Lattices
   160.8 +imports Countable_Set Cardinal_Notations HOL.Conditionally_Complete_Lattices
   160.9  begin
  160.10  
  160.11  
   161.1 --- a/src/HOL/Library/FuncSet.thy	Fri Aug 18 14:57:23 2017 +0200
   161.2 +++ b/src/HOL/Library/FuncSet.thy	Fri Aug 18 22:55:54 2017 +0200
   161.3 @@ -5,7 +5,7 @@
   161.4  section \<open>Pi and Function Sets\<close>
   161.5  
   161.6  theory FuncSet
   161.7 -  imports Hilbert_Choice Main
   161.8 +  imports HOL.Hilbert_Choice Main
   161.9    abbrevs PiE = "Pi\<^sub>E"
  161.10      PIE = "\<Pi>\<^sub>E"
  161.11  begin
   162.1 --- a/src/HOL/Library/Lattice_Syntax.thy	Fri Aug 18 14:57:23 2017 +0200
   162.2 +++ b/src/HOL/Library/Lattice_Syntax.thy	Fri Aug 18 22:55:54 2017 +0200
   162.3 @@ -3,7 +3,7 @@
   162.4  section \<open>Pretty syntax for lattice operations\<close>
   162.5  
   162.6  theory Lattice_Syntax
   162.7 -imports Complete_Lattices
   162.8 +imports HOL.Complete_Lattices
   162.9  begin
  162.10  
  162.11  notation
   163.1 --- a/src/HOL/Library/ListVector.thy	Fri Aug 18 14:57:23 2017 +0200
   163.2 +++ b/src/HOL/Library/ListVector.thy	Fri Aug 18 22:55:54 2017 +0200
   163.3 @@ -3,7 +3,7 @@
   163.4  section \<open>Lists as vectors\<close>
   163.5  
   163.6  theory ListVector
   163.7 -imports List Main
   163.8 +imports HOL.List Main
   163.9  begin
  163.10  
  163.11  text\<open>\noindent
   164.1 --- a/src/HOL/Library/Option_ord.thy	Fri Aug 18 14:57:23 2017 +0200
   164.2 +++ b/src/HOL/Library/Option_ord.thy	Fri Aug 18 22:55:54 2017 +0200
   164.3 @@ -5,7 +5,7 @@
   164.4  section \<open>Canonical order on option type\<close>
   164.5  
   164.6  theory Option_ord
   164.7 -imports Option Main
   164.8 +imports HOL.Option Main
   164.9  begin
  164.10  
  164.11  notation
   165.1 --- a/src/HOL/Library/Preorder.thy	Fri Aug 18 14:57:23 2017 +0200
   165.2 +++ b/src/HOL/Library/Preorder.thy	Fri Aug 18 22:55:54 2017 +0200
   165.3 @@ -3,7 +3,7 @@
   165.4  section \<open>Preorders with explicit equivalence relation\<close>
   165.5  
   165.6  theory Preorder
   165.7 -imports Orderings
   165.8 +imports HOL.Orderings
   165.9  begin
  165.10  
  165.11  class preorder_equiv = preorder
   166.1 --- a/src/HOL/Matrix_LP/ComputeFloat.thy	Fri Aug 18 14:57:23 2017 +0200
   166.2 +++ b/src/HOL/Matrix_LP/ComputeFloat.thy	Fri Aug 18 22:55:54 2017 +0200
   166.3 @@ -5,7 +5,7 @@
   166.4  section \<open>Floating Point Representation of the Reals\<close>
   166.5  
   166.6  theory ComputeFloat
   166.7 -imports Complex_Main "~~/src/HOL/Library/Lattice_Algebras"
   166.8 +imports Complex_Main "HOL-Library.Lattice_Algebras"
   166.9  begin
  166.10  
  166.11  ML_file "~~/src/Tools/float.ML"
   167.1 --- a/src/HOL/Matrix_LP/Compute_Oracle/Compute_Oracle.thy	Fri Aug 18 14:57:23 2017 +0200
   167.2 +++ b/src/HOL/Matrix_LP/Compute_Oracle/Compute_Oracle.thy	Fri Aug 18 22:55:54 2017 +0200
   167.3 @@ -4,7 +4,7 @@
   167.4  Steven Obua's evaluator.
   167.5  *)
   167.6  
   167.7 -theory Compute_Oracle imports HOL
   167.8 +theory Compute_Oracle imports HOL.HOL
   167.9  begin
  167.10  
  167.11  ML_file "am.ML"
   168.1 --- a/src/HOL/Matrix_LP/LP.thy	Fri Aug 18 14:57:23 2017 +0200
   168.2 +++ b/src/HOL/Matrix_LP/LP.thy	Fri Aug 18 22:55:54 2017 +0200
   168.3 @@ -3,7 +3,7 @@
   168.4  *)
   168.5  
   168.6  theory LP 
   168.7 -imports Main "~~/src/HOL/Library/Lattice_Algebras"
   168.8 +imports Main "HOL-Library.Lattice_Algebras"
   168.9  begin
  168.10  
  168.11  lemma le_add_right_mono: 
   169.1 --- a/src/HOL/Matrix_LP/Matrix.thy	Fri Aug 18 14:57:23 2017 +0200
   169.2 +++ b/src/HOL/Matrix_LP/Matrix.thy	Fri Aug 18 22:55:54 2017 +0200
   169.3 @@ -3,7 +3,7 @@
   169.4  *)
   169.5  
   169.6  theory Matrix
   169.7 -imports Main "~~/src/HOL/Library/Lattice_Algebras"
   169.8 +imports Main "HOL-Library.Lattice_Algebras"
   169.9  begin
  169.10  
  169.11  type_synonym 'a infmatrix = "nat \<Rightarrow> nat \<Rightarrow> 'a"
   170.1 --- a/src/HOL/Metis_Examples/Abstraction.thy	Fri Aug 18 14:57:23 2017 +0200
   170.2 +++ b/src/HOL/Metis_Examples/Abstraction.thy	Fri Aug 18 22:55:54 2017 +0200
   170.3 @@ -8,7 +8,7 @@
   170.4  section \<open>Example Featuring Metis's Support for Lambda-Abstractions\<close>
   170.5  
   170.6  theory Abstraction
   170.7 -imports "~~/src/HOL/Library/FuncSet"
   170.8 +imports "HOL-Library.FuncSet"
   170.9  begin
  170.10  
  170.11  (* For Christoph Benzmüller *)
   171.1 --- a/src/HOL/Metis_Examples/Big_O.thy	Fri Aug 18 14:57:23 2017 +0200
   171.2 +++ b/src/HOL/Metis_Examples/Big_O.thy	Fri Aug 18 22:55:54 2017 +0200
   171.3 @@ -9,9 +9,9 @@
   171.4  
   171.5  theory Big_O
   171.6  imports
   171.7 -  "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
   171.8 -  "~~/src/HOL/Library/Function_Algebras"
   171.9 -  "~~/src/HOL/Library/Set_Algebras"
  171.10 +  "HOL-Decision_Procs.Dense_Linear_Order"
  171.11 +  "HOL-Library.Function_Algebras"
  171.12 +  "HOL-Library.Set_Algebras"
  171.13  begin
  171.14  
  171.15  subsection \<open>Definitions\<close>
   172.1 --- a/src/HOL/Metis_Examples/Tarski.thy	Fri Aug 18 14:57:23 2017 +0200
   172.2 +++ b/src/HOL/Metis_Examples/Tarski.thy	Fri Aug 18 22:55:54 2017 +0200
   172.3 @@ -8,7 +8,7 @@
   172.4  section \<open>Metis Example Featuring the Full Theorem of Tarski\<close>
   172.5  
   172.6  theory Tarski
   172.7 -imports Main "~~/src/HOL/Library/FuncSet"
   172.8 +imports Main "HOL-Library.FuncSet"
   172.9  begin
  172.10  
  172.11  declare [[metis_new_skolem]]
   173.1 --- a/src/HOL/MicroJava/DFA/Kildall.thy	Fri Aug 18 14:57:23 2017 +0200
   173.2 +++ b/src/HOL/MicroJava/DFA/Kildall.thy	Fri Aug 18 22:55:54 2017 +0200
   173.3 @@ -6,7 +6,7 @@
   173.4  section \<open>Kildall's Algorithm \label{sec:Kildall}\<close>
   173.5  
   173.6  theory Kildall
   173.7 -imports SemilatAlg "~~/src/HOL/Library/While_Combinator"
   173.8 +imports SemilatAlg "HOL-Library.While_Combinator"
   173.9  begin
  173.10  
  173.11  primrec propa :: "'s binop \<Rightarrow> (nat \<times> 's) list \<Rightarrow> 's list \<Rightarrow> nat set \<Rightarrow> 's list * nat set" where
   174.1 --- a/src/HOL/MicroJava/DFA/Semilat.thy	Fri Aug 18 14:57:23 2017 +0200
   174.2 +++ b/src/HOL/MicroJava/DFA/Semilat.thy	Fri Aug 18 22:55:54 2017 +0200
   174.3 @@ -8,7 +8,7 @@
   174.4  section \<open>Semilattices\<close>
   174.5  
   174.6  theory Semilat
   174.7 -imports Main "~~/src/HOL/Library/While_Combinator"
   174.8 +imports Main "HOL-Library.While_Combinator"
   174.9  begin
  174.10  
  174.11  type_synonym 'a ord = "'a \<Rightarrow> 'a \<Rightarrow> bool"
   175.1 --- a/src/HOL/MicroJava/J/JBasis.thy	Fri Aug 18 14:57:23 2017 +0200
   175.2 +++ b/src/HOL/MicroJava/J/JBasis.thy	Fri Aug 18 22:55:54 2017 +0200
   175.3 @@ -9,8 +9,8 @@
   175.4  theory JBasis
   175.5  imports
   175.6    Main
   175.7 -  "~~/src/HOL/Library/Transitive_Closure_Table"
   175.8 -  "~~/src/HOL/Eisbach/Eisbach"
   175.9 +  "HOL-Library.Transitive_Closure_Table"
  175.10 +  "HOL-Eisbach.Eisbach"
  175.11  begin
  175.12  
  175.13  lemmas [simp] = Let_def
   176.1 --- a/src/HOL/Mutabelle/MutabelleExtra.thy	Fri Aug 18 14:57:23 2017 +0200
   176.2 +++ b/src/HOL/Mutabelle/MutabelleExtra.thy	Fri Aug 18 22:55:54 2017 +0200
   176.3 @@ -1,5 +1,5 @@
   176.4  theory MutabelleExtra
   176.5 -imports Complex_Main "~~/src/HOL/Library/Refute"
   176.6 +imports Complex_Main "HOL-Library.Refute"
   176.7  (*  "~/repos/afp/thys/AVL-Trees/AVL"
   176.8    "~/repos/afp/thys/BinarySearchTree/BinaryTree"
   176.9    "~/repos/afp/thys/Huffman/Huffman"
   177.1 --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Fri Aug 18 14:57:23 2017 +0200
   177.2 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Fri Aug 18 22:55:54 2017 +0200
   177.3 @@ -12,7 +12,7 @@
   177.4     suite. *)
   177.5  
   177.6  theory Manual_Nits
   177.7 -imports Real "~~/src/HOL/Library/Quotient_Product"
   177.8 +imports HOL.Real "HOL-Library.Quotient_Product"
   177.9  begin
  177.10  
  177.11  section \<open>2. First Steps\<close>
   178.1 --- a/src/HOL/Nominal/Examples/CK_Machine.thy	Fri Aug 18 14:57:23 2017 +0200
   178.2 +++ b/src/HOL/Nominal/Examples/CK_Machine.thy	Fri Aug 18 22:55:54 2017 +0200
   178.3 @@ -1,5 +1,5 @@
   178.4  theory CK_Machine 
   178.5 -  imports "../Nominal" 
   178.6 +  imports "HOL-Nominal.Nominal" 
   178.7  begin
   178.8  
   178.9  text \<open>
   179.1 --- a/src/HOL/Nominal/Examples/CR_Takahashi.thy	Fri Aug 18 14:57:23 2017 +0200
   179.2 +++ b/src/HOL/Nominal/Examples/CR_Takahashi.thy	Fri Aug 18 22:55:54 2017 +0200
   179.3 @@ -8,7 +8,7 @@
   179.4  (*  Church-Rosser Theorem (1995).                                 *)
   179.5  
   179.6  theory CR_Takahashi
   179.7 -  imports "../Nominal"
   179.8 +  imports "HOL-Nominal.Nominal"
   179.9  begin
  179.10  
  179.11  atom_decl name
   180.1 --- a/src/HOL/Nominal/Examples/Class1.thy	Fri Aug 18 14:57:23 2017 +0200
   180.2 +++ b/src/HOL/Nominal/Examples/Class1.thy	Fri Aug 18 22:55:54 2017 +0200
   180.3 @@ -1,5 +1,5 @@
   180.4  theory Class1
   180.5 -imports "../Nominal" 
   180.6 +imports "HOL-Nominal.Nominal" 
   180.7  begin
   180.8  
   180.9  section \<open>Term-Calculus from Urban's PhD\<close>
   181.1 --- a/src/HOL/Nominal/Examples/Compile.thy	Fri Aug 18 14:57:23 2017 +0200
   181.2 +++ b/src/HOL/Nominal/Examples/Compile.thy	Fri Aug 18 22:55:54 2017 +0200
   181.3 @@ -1,7 +1,7 @@
   181.4  (* The definitions for a challenge suggested by Adam Chlipala *)
   181.5  
   181.6  theory Compile
   181.7 -imports "../Nominal"
   181.8 +imports "HOL-Nominal.Nominal"
   181.9  begin
  181.10  
  181.11  atom_decl name 
   182.1 --- a/src/HOL/Nominal/Examples/Contexts.thy	Fri Aug 18 14:57:23 2017 +0200
   182.2 +++ b/src/HOL/Nominal/Examples/Contexts.thy	Fri Aug 18 22:55:54 2017 +0200
   182.3 @@ -1,5 +1,5 @@
   182.4  theory Contexts
   182.5 -imports "../Nominal"
   182.6 +imports "HOL-Nominal.Nominal"
   182.7  begin
   182.8  
   182.9  text \<open>
   183.1 --- a/src/HOL/Nominal/Examples/Crary.thy	Fri Aug 18 14:57:23 2017 +0200
   183.2 +++ b/src/HOL/Nominal/Examples/Crary.thy	Fri Aug 18 22:55:54 2017 +0200
   183.3 @@ -8,7 +8,7 @@
   183.4  (* Christian Urban.                                   *)
   183.5  
   183.6  theory Crary
   183.7 -  imports "../Nominal"
   183.8 +  imports "HOL-Nominal.Nominal"
   183.9  begin
  183.10  
  183.11  atom_decl name 
   184.1 --- a/src/HOL/Nominal/Examples/Fsub.thy	Fri Aug 18 14:57:23 2017 +0200
   184.2 +++ b/src/HOL/Nominal/Examples/Fsub.thy	Fri Aug 18 22:55:54 2017 +0200
   184.3 @@ -1,6 +1,6 @@
   184.4  (*<*)
   184.5  theory Fsub
   184.6 -imports "../Nominal" 
   184.7 +imports "HOL-Nominal.Nominal" 
   184.8  begin
   184.9  (*>*)
  184.10  
   185.1 --- a/src/HOL/Nominal/Examples/Height.thy	Fri Aug 18 14:57:23 2017 +0200
   185.2 +++ b/src/HOL/Nominal/Examples/Height.thy	Fri Aug 18 22:55:54 2017 +0200
   185.3 @@ -1,5 +1,5 @@
   185.4  theory Height
   185.5 -  imports "../Nominal"
   185.6 +  imports "HOL-Nominal.Nominal"
   185.7  begin
   185.8  
   185.9  text \<open>
   186.1 --- a/src/HOL/Nominal/Examples/Lam_Funs.thy	Fri Aug 18 14:57:23 2017 +0200
   186.2 +++ b/src/HOL/Nominal/Examples/Lam_Funs.thy	Fri Aug 18 22:55:54 2017 +0200
   186.3 @@ -1,5 +1,5 @@
   186.4  theory Lam_Funs
   186.5 -  imports "../Nominal"
   186.6 +  imports "HOL-Nominal.Nominal"
   186.7  begin
   186.8  
   186.9  text \<open>
   187.1 --- a/src/HOL/Nominal/Examples/Lambda_mu.thy	Fri Aug 18 14:57:23 2017 +0200
   187.2 +++ b/src/HOL/Nominal/Examples/Lambda_mu.thy	Fri Aug 18 22:55:54 2017 +0200
   187.3 @@ -1,5 +1,5 @@
   187.4  theory Lambda_mu 
   187.5 -  imports "../Nominal" 
   187.6 +  imports "HOL-Nominal.Nominal" 
   187.7  begin
   187.8  
   187.9  section \<open>Lambda-Mu according to a paper by Gavin Bierman\<close>
   188.1 --- a/src/HOL/Nominal/Examples/LocalWeakening.thy	Fri Aug 18 14:57:23 2017 +0200
   188.2 +++ b/src/HOL/Nominal/Examples/LocalWeakening.thy	Fri Aug 18 22:55:54 2017 +0200
   188.3 @@ -4,7 +4,7 @@
   188.4  (*                                                      *)
   188.5  (* Authors: Christian Urban and Randy Pollack           *)
   188.6  theory LocalWeakening
   188.7 -  imports "../Nominal"
   188.8 +  imports "HOL-Nominal.Nominal"
   188.9  begin
  188.10  
  188.11  atom_decl name
   189.1 --- a/src/HOL/Nominal/Examples/Pattern.thy	Fri Aug 18 14:57:23 2017 +0200
   189.2 +++ b/src/HOL/Nominal/Examples/Pattern.thy	Fri Aug 18 22:55:54 2017 +0200
   189.3 @@ -1,7 +1,7 @@
   189.4  section \<open>Simply-typed lambda-calculus with let and tuple patterns\<close>
   189.5  
   189.6  theory Pattern
   189.7 -imports "../Nominal"
   189.8 +imports "HOL-Nominal.Nominal"
   189.9  begin
  189.10  
  189.11  no_syntax
   190.1 --- a/src/HOL/Nominal/Examples/SOS.thy	Fri Aug 18 14:57:23 2017 +0200
   190.2 +++ b/src/HOL/Nominal/Examples/SOS.thy	Fri Aug 18 22:55:54 2017 +0200
   190.3 @@ -11,7 +11,7 @@
   190.4  (* Christian Urban.                                       *)
   190.5  
   190.6  theory SOS
   190.7 -  imports "../Nominal"
   190.8 +  imports "HOL-Nominal.Nominal"
   190.9  begin
  190.10  
  190.11  atom_decl name
   191.1 --- a/src/HOL/Nominal/Examples/Standardization.thy	Fri Aug 18 14:57:23 2017 +0200
   191.2 +++ b/src/HOL/Nominal/Examples/Standardization.thy	Fri Aug 18 22:55:54 2017 +0200
   191.3 @@ -6,7 +6,7 @@
   191.4  section \<open>Standardization\<close>
   191.5  
   191.6  theory Standardization
   191.7 -imports "../Nominal"
   191.8 +imports "HOL-Nominal.Nominal"
   191.9  begin
  191.10  
  191.11  text \<open>
   192.1 --- a/src/HOL/Nominal/Examples/Support.thy	Fri Aug 18 14:57:23 2017 +0200
   192.2 +++ b/src/HOL/Nominal/Examples/Support.thy	Fri Aug 18 22:55:54 2017 +0200
   192.3 @@ -1,5 +1,5 @@
   192.4  theory Support 
   192.5 -  imports "../Nominal" 
   192.6 +  imports "HOL-Nominal.Nominal" 
   192.7  begin
   192.8  
   192.9  text \<open>
   193.1 --- a/src/HOL/Nominal/Examples/Type_Preservation.thy	Fri Aug 18 14:57:23 2017 +0200
   193.2 +++ b/src/HOL/Nominal/Examples/Type_Preservation.thy	Fri Aug 18 22:55:54 2017 +0200
   193.3 @@ -1,5 +1,5 @@
   193.4  theory Type_Preservation
   193.5 -  imports "../Nominal"
   193.6 +  imports "HOL-Nominal.Nominal"
   193.7  begin
   193.8  
   193.9  text \<open>
   194.1 --- a/src/HOL/Nominal/Examples/VC_Condition.thy	Fri Aug 18 14:57:23 2017 +0200
   194.2 +++ b/src/HOL/Nominal/Examples/VC_Condition.thy	Fri Aug 18 22:55:54 2017 +0200
   194.3 @@ -1,5 +1,5 @@
   194.4  theory VC_Condition
   194.5 -imports "../Nominal" 
   194.6 +imports "HOL-Nominal.Nominal" 
   194.7  begin
   194.8  
   194.9  text \<open>
   195.1 --- a/src/HOL/Nominal/Examples/W.thy	Fri Aug 18 14:57:23 2017 +0200
   195.2 +++ b/src/HOL/Nominal/Examples/W.thy	Fri Aug 18 22:55:54 2017 +0200
   195.3 @@ -1,5 +1,5 @@
   195.4  theory W
   195.5 -imports "../Nominal"
   195.6 +imports "HOL-Nominal.Nominal"
   195.7  begin
   195.8  
   195.9  text \<open>Example for strong induction rules avoiding sets of atoms.\<close>
   196.1 --- a/src/HOL/Nominal/Examples/Weakening.thy	Fri Aug 18 14:57:23 2017 +0200
   196.2 +++ b/src/HOL/Nominal/Examples/Weakening.thy	Fri Aug 18 22:55:54 2017 +0200
   196.3 @@ -1,5 +1,5 @@
   196.4  theory Weakening 
   196.5 -  imports "../Nominal" 
   196.6 +  imports "HOL-Nominal.Nominal" 
   196.7  begin
   196.8  
   196.9  text \<open>
   197.1 --- a/src/HOL/Nominal/Nominal.thy	Fri Aug 18 14:57:23 2017 +0200
   197.2 +++ b/src/HOL/Nominal/Nominal.thy	Fri Aug 18 22:55:54 2017 +0200
   197.3 @@ -1,5 +1,5 @@
   197.4  theory Nominal 
   197.5 -imports "~~/src/HOL/Library/Infinite_Set" "~~/src/HOL/Library/Old_Datatype"
   197.6 +imports "HOL-Library.Infinite_Set" "HOL-Library.Old_Datatype"
   197.7  keywords
   197.8    "atom_decl" "nominal_datatype" "equivariance" :: thy_decl and
   197.9    "nominal_primrec" "nominal_inductive" "nominal_inductive2" :: thy_goal and
   198.1 --- a/src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy	Fri Aug 18 14:57:23 2017 +0200
   198.2 +++ b/src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy	Fri Aug 18 22:55:54 2017 +0200
   198.3 @@ -7,7 +7,7 @@
   198.4  section \<open>The Nonstandard Primes as an Extension of the Prime Numbers\<close>
   198.5  
   198.6  theory NSPrimes
   198.7 -  imports "~~/src/HOL/Computational_Algebra/Primes" "../Hyperreal"
   198.8 +  imports "HOL-Computational_Algebra.Primes" "HOL-Nonstandard_Analysis.Hyperreal"
   198.9  begin
  198.10  
  198.11  text \<open>These can be used to derive an alternative proof of the infinitude of
   199.1 --- a/src/HOL/Nonstandard_Analysis/Free_Ultrafilter.thy	Fri Aug 18 14:57:23 2017 +0200
   199.2 +++ b/src/HOL/Nonstandard_Analysis/Free_Ultrafilter.thy	Fri Aug 18 22:55:54 2017 +0200
   199.3 @@ -7,7 +7,7 @@
   199.4  section \<open>Filters and Ultrafilters\<close>
   199.5  
   199.6  theory Free_Ultrafilter
   199.7 -  imports "~~/src/HOL/Library/Infinite_Set"
   199.8 +  imports "HOL-Library.Infinite_Set"
   199.9  begin
  199.10  
  199.11  
   200.1 --- a/src/HOL/Nonstandard_Analysis/HSEQ.thy	Fri Aug 18 14:57:23 2017 +0200
   200.2 +++ b/src/HOL/Nonstandard_Analysis/HSEQ.thy	Fri Aug 18 22:55:54 2017 +0200
   200.3 @@ -11,7 +11,7 @@
   200.4  section \<open>Sequences and Convergence (Nonstandard)\<close>
   200.5  
   200.6  theory HSEQ
   200.7 -  imports Limits NatStar
   200.8 +  imports HOL.Limits NatStar
   200.9    abbrevs "--->" = "\<longlonglongrightarrow>\<^sub>N\<^sub>S"
  200.10  begin
  200.11  
   201.1 --- a/src/HOL/Nonstandard_Analysis/HTranscendental.thy	Fri Aug 18 14:57:23 2017 +0200
   201.2 +++ b/src/HOL/Nonstandard_Analysis/HTranscendental.thy	Fri Aug 18 22:55:54 2017 +0200
   201.3 @@ -8,7 +8,7 @@
   201.4  section\<open>Nonstandard Extensions of Transcendental Functions\<close>
   201.5  
   201.6  theory HTranscendental
   201.7 -imports Transcendental HSeries HDeriv
   201.8 +imports HOL.Transcendental HSeries HDeriv
   201.9  begin
  201.10  
  201.11  definition
   202.1 --- a/src/HOL/Nonstandard_Analysis/NSA.thy	Fri Aug 18 14:57:23 2017 +0200
   202.2 +++ b/src/HOL/Nonstandard_Analysis/NSA.thy	Fri Aug 18 22:55:54 2017 +0200
   202.3 @@ -6,7 +6,7 @@
   202.4  section \<open>Infinite Numbers, Infinitesimals, Infinitely Close Relation\<close>
   202.5  
   202.6  theory NSA
   202.7 -  imports HyperDef "~~/src/HOL/Library/Lub_Glb"
   202.8 +  imports HyperDef "HOL-Library.Lub_Glb"
   202.9  begin
  202.10  
  202.11  definition hnorm :: "'a::real_normed_vector star \<Rightarrow> real star"
   203.1 --- a/src/HOL/Number_Theory/Cong.thy	Fri Aug 18 14:57:23 2017 +0200
   203.2 +++ b/src/HOL/Number_Theory/Cong.thy	Fri Aug 18 22:55:54 2017 +0200
   203.3 @@ -29,7 +29,7 @@
   203.4  section \<open>Congruence\<close>
   203.5  
   203.6  theory Cong
   203.7 -  imports "~~/src/HOL/Computational_Algebra/Primes"
   203.8 +  imports "HOL-Computational_Algebra.Primes"
   203.9  begin
  203.10  
  203.11  subsection \<open>Turn off \<open>One_nat_def\<close>\<close>
   204.1 --- a/src/HOL/Number_Theory/Eratosthenes.thy	Fri Aug 18 14:57:23 2017 +0200
   204.2 +++ b/src/HOL/Number_Theory/Eratosthenes.thy	Fri Aug 18 22:55:54 2017 +0200
   204.3 @@ -5,7 +5,7 @@
   204.4  section \<open>The sieve of Eratosthenes\<close>
   204.5  
   204.6  theory Eratosthenes
   204.7 -  imports Main "~~/src/HOL/Computational_Algebra/Primes"
   204.8 +  imports Main "HOL-Computational_Algebra.Primes"
   204.9  begin
  204.10  
  204.11  
   205.1 --- a/src/HOL/Number_Theory/Prime_Powers.thy	Fri Aug 18 14:57:23 2017 +0200
   205.2 +++ b/src/HOL/Number_Theory/Prime_Powers.thy	Fri Aug 18 22:55:54 2017 +0200
   205.3 @@ -6,7 +6,7 @@
   205.4  *)
   205.5  section \<open>Prime powers\<close>
   205.6  theory Prime_Powers
   205.7 -  imports Complex_Main "~~/src/HOL/Computational_Algebra/Primes"
   205.8 +  imports Complex_Main "HOL-Computational_Algebra.Primes"
   205.9  begin
  205.10  
  205.11  definition aprimedivisor :: "'a :: normalization_semidom \<Rightarrow> 'a" where
   206.1 --- a/src/HOL/Number_Theory/Residues.thy	Fri Aug 18 14:57:23 2017 +0200
   206.2 +++ b/src/HOL/Number_Theory/Residues.thy	Fri Aug 18 22:55:54 2017 +0200
   206.3 @@ -10,10 +10,10 @@
   206.4  theory Residues
   206.5  imports
   206.6    Cong
   206.7 -  "~~/src/HOL/Algebra/More_Group"
   206.8 -  "~~/src/HOL/Algebra/More_Ring"
   206.9 -  "~~/src/HOL/Algebra/More_Finite_Product"
  206.10 -  "~~/src/HOL/Algebra/Multiplicative_Group"
  206.11 +  "HOL-Algebra.More_Group"
  206.12 +  "HOL-Algebra.More_Ring"
  206.13 +  "HOL-Algebra.More_Finite_Product"
  206.14 +  "HOL-Algebra.Multiplicative_Group"
  206.15    Totient
  206.16  begin
  206.17  
   207.1 --- a/src/HOL/Number_Theory/Totient.thy	Fri Aug 18 14:57:23 2017 +0200
   207.2 +++ b/src/HOL/Number_Theory/Totient.thy	Fri Aug 18 22:55:54 2017 +0200
   207.3 @@ -9,7 +9,7 @@
   207.4  theory Totient
   207.5  imports
   207.6    Complex_Main
   207.7 -  "~~/src/HOL/Computational_Algebra/Primes"
   207.8 +  "HOL-Computational_Algebra.Primes"
   207.9    "~~/src/HOL/Number_Theory/Cong"
  207.10  begin
  207.11    
   208.1 --- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Fri Aug 18 14:57:23 2017 +0200
   208.2 +++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Fri Aug 18 22:55:54 2017 +0200
   208.3 @@ -1,5 +1,5 @@
   208.4  theory Code_Prolog_Examples
   208.5 -imports "~~/src/HOL/Library/Code_Prolog"
   208.6 +imports "HOL-Library.Code_Prolog"
   208.7  begin
   208.8  
   208.9  section \<open>Example append\<close>
   209.1 --- a/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	Fri Aug 18 14:57:23 2017 +0200
   209.2 +++ b/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	Fri Aug 18 22:55:54 2017 +0200
   209.3 @@ -1,5 +1,5 @@
   209.4  theory Context_Free_Grammar_Example
   209.5 -imports "~~/src/HOL/Library/Code_Prolog"
   209.6 +imports "HOL-Library.Code_Prolog"
   209.7  begin
   209.8  (*
   209.9  declare mem_def[code_pred_inline]
   210.1 --- a/src/HOL/Predicate_Compile_Examples/Examples.thy	Fri Aug 18 14:57:23 2017 +0200
   210.2 +++ b/src/HOL/Predicate_Compile_Examples/Examples.thy	Fri Aug 18 22:55:54 2017 +0200
   210.3 @@ -1,5 +1,5 @@
   210.4  theory Examples
   210.5 -imports Main "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs"
   210.6 +imports Main "HOL-Library.Predicate_Compile_Alternative_Defs"
   210.7  begin
   210.8  
   210.9  declare [[values_timeout = 480.0]]
   211.1 --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	Fri Aug 18 14:57:23 2017 +0200
   211.2 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	Fri Aug 18 22:55:54 2017 +0200
   211.3 @@ -1,8 +1,8 @@
   211.4  theory Hotel_Example_Prolog
   211.5  imports
   211.6    Hotel_Example
   211.7 -  "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs"
   211.8 -  "~~/src/HOL/Library/Code_Prolog"
   211.9 +  "HOL-Library.Predicate_Compile_Alternative_Defs"
  211.10 +  "HOL-Library.Code_Prolog"
  211.11  begin
  211.12  
  211.13  declare Let_def[code_pred_inline]
   212.1 --- a/src/HOL/Predicate_Compile_Examples/IMP_1.thy	Fri Aug 18 14:57:23 2017 +0200
   212.2 +++ b/src/HOL/Predicate_Compile_Examples/IMP_1.thy	Fri Aug 18 22:55:54 2017 +0200
   212.3 @@ -1,5 +1,5 @@
   212.4  theory IMP_1
   212.5 -imports "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
   212.6 +imports "HOL-Library.Predicate_Compile_Quickcheck"
   212.7  begin
   212.8  
   212.9  subsection \<open>IMP\<close>
   213.1 --- a/src/HOL/Predicate_Compile_Examples/IMP_2.thy	Fri Aug 18 14:57:23 2017 +0200
   213.2 +++ b/src/HOL/Predicate_Compile_Examples/IMP_2.thy	Fri Aug 18 22:55:54 2017 +0200
   213.3 @@ -1,5 +1,5 @@
   213.4  theory IMP_2
   213.5 -imports "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
   213.6 +imports "HOL-Library.Predicate_Compile_Quickcheck"
   213.7  begin
   213.8  
   213.9  subsection \<open>IMP\<close>
   214.1 --- a/src/HOL/Predicate_Compile_Examples/IMP_3.thy	Fri Aug 18 14:57:23 2017 +0200
   214.2 +++ b/src/HOL/Predicate_Compile_Examples/IMP_3.thy	Fri Aug 18 22:55:54 2017 +0200
   214.3 @@ -1,5 +1,5 @@
   214.4  theory IMP_3
   214.5 -imports "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
   214.6 +imports "HOL-Library.Predicate_Compile_Quickcheck"
   214.7  begin
   214.8  
   214.9  subsection \<open>IMP\<close>
   215.1 --- a/src/HOL/Predicate_Compile_Examples/IMP_4.thy	Fri Aug 18 14:57:23 2017 +0200
   215.2 +++ b/src/HOL/Predicate_Compile_Examples/IMP_4.thy	Fri Aug 18 22:55:54 2017 +0200
   215.3 @@ -1,5 +1,5 @@
   215.4  theory IMP_4
   215.5 -imports "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
   215.6 +imports "HOL-Library.Predicate_Compile_Quickcheck"
   215.7  begin
   215.8  
   215.9  subsection \<open>IMP\<close>
   216.1 --- a/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy	Fri Aug 18 14:57:23 2017 +0200
   216.2 +++ b/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy	Fri Aug 18 22:55:54 2017 +0200
   216.3 @@ -1,5 +1,5 @@
   216.4  theory Lambda_Example
   216.5 -imports "~~/src/HOL/Library/Code_Prolog"
   216.6 +imports "HOL-Library.Code_Prolog"
   216.7  begin
   216.8  
   216.9  subsection \<open>Lambda\<close>
   217.1 --- a/src/HOL/Predicate_Compile_Examples/List_Examples.thy	Fri Aug 18 14:57:23 2017 +0200
   217.2 +++ b/src/HOL/Predicate_Compile_Examples/List_Examples.thy	Fri Aug 18 22:55:54 2017 +0200
   217.3 @@ -1,8 +1,8 @@
   217.4  theory List_Examples
   217.5  imports
   217.6    Main
   217.7 -  "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
   217.8 -  "~~/src/HOL/Library/Code_Prolog"
   217.9 +  "HOL-Library.Predicate_Compile_Quickcheck"
  217.10 +  "HOL-Library.Code_Prolog"
  217.11  begin
  217.12  
  217.13  setup \<open>
   218.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Fri Aug 18 14:57:23 2017 +0200
   218.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Fri Aug 18 22:55:54 2017 +0200
   218.3 @@ -1,5 +1,5 @@
   218.4  theory Predicate_Compile_Quickcheck_Examples
   218.5 -imports "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
   218.6 +imports "HOL-Library.Predicate_Compile_Quickcheck"
   218.7  begin
   218.8  
   218.9  (*
   219.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Fri Aug 18 14:57:23 2017 +0200
   219.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Fri Aug 18 22:55:54 2017 +0200
   219.3 @@ -1,5 +1,5 @@
   219.4  theory Predicate_Compile_Tests
   219.5 -imports "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs"
   219.6 +imports "HOL-Library.Predicate_Compile_Alternative_Defs"
   219.7  begin
   219.8  
   219.9  declare [[values_timeout = 480.0]]
   220.1 --- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Fri Aug 18 14:57:23 2017 +0200
   220.2 +++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Fri Aug 18 22:55:54 2017 +0200
   220.3 @@ -1,7 +1,7 @@
   220.4  theory Reg_Exp_Example
   220.5  imports
   220.6 -  "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
   220.7 -  "~~/src/HOL/Library/Code_Prolog"
   220.8 +  "HOL-Library.Predicate_Compile_Quickcheck"
   220.9 +  "HOL-Library.Code_Prolog"
  220.10  begin
  220.11  
  220.12  text \<open>An example from the experiments from SmallCheck (\<^url>\<open>http://www.cs.york.ac.uk/fp/smallcheck\<close>)\<close>
   221.1 --- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Fri Aug 18 14:57:23 2017 +0200
   221.2 +++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Fri Aug 18 22:55:54 2017 +0200
   221.3 @@ -1,5 +1,5 @@
   221.4  theory Specialisation_Examples
   221.5 -imports Main "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs"
   221.6 +imports Main "HOL-Library.Predicate_Compile_Alternative_Defs"
   221.7  begin
   221.8  
   221.9  declare [[values_timeout = 960.0]]
   222.1 --- a/src/HOL/Probability/Discrete_Topology.thy	Fri Aug 18 14:57:23 2017 +0200
   222.2 +++ b/src/HOL/Probability/Discrete_Topology.thy	Fri Aug 18 22:55:54 2017 +0200
   222.3 @@ -3,7 +3,7 @@
   222.4  *)
   222.5  
   222.6  theory Discrete_Topology
   222.7 -imports "~~/src/HOL/Analysis/Analysis"
   222.8 +imports "HOL-Analysis.Analysis"
   222.9  begin
  222.10  
  222.11  text \<open>Copy of discrete types with discrete topology. This space is polish.\<close>
   223.1 --- a/src/HOL/Probability/Essential_Supremum.thy	Fri Aug 18 14:57:23 2017 +0200
   223.2 +++ b/src/HOL/Probability/Essential_Supremum.thy	Fri Aug 18 22:55:54 2017 +0200
   223.3 @@ -4,7 +4,7 @@
   223.4  *)
   223.5  
   223.6  theory Essential_Supremum
   223.7 -imports "../Analysis/Analysis"
   223.8 +imports "HOL-Analysis.Analysis"
   223.9  begin
  223.10  
  223.11  lemma ae_filter_eq_bot_iff: "ae_filter M = bot \<longleftrightarrow> emeasure M (space M) = 0"
   224.1 --- a/src/HOL/Probability/Fin_Map.thy	Fri Aug 18 14:57:23 2017 +0200
   224.2 +++ b/src/HOL/Probability/Fin_Map.thy	Fri Aug 18 22:55:54 2017 +0200
   224.3 @@ -5,7 +5,7 @@
   224.4  section \<open>Finite Maps\<close>
   224.5  
   224.6  theory Fin_Map
   224.7 -  imports "~~/src/HOL/Analysis/Finite_Product_Measure" "~~/src/HOL/Library/Finite_Map"
   224.8 +  imports "HOL-Analysis.Finite_Product_Measure" "HOL-Library.Finite_Map"
   224.9  begin
  224.10  
  224.11  text \<open>The @{type fmap} type can be instantiated to @{class polish_space}, needed for the proof of
   225.1 --- a/src/HOL/Probability/Giry_Monad.thy	Fri Aug 18 14:57:23 2017 +0200
   225.2 +++ b/src/HOL/Probability/Giry_Monad.thy	Fri Aug 18 22:55:54 2017 +0200
   225.3 @@ -7,7 +7,7 @@
   225.4  *)
   225.5  
   225.6  theory Giry_Monad
   225.7 -  imports Probability_Measure "~~/src/HOL/Library/Monad_Syntax"
   225.8 +  imports Probability_Measure "HOL-Library.Monad_Syntax"
   225.9  begin
  225.10  
  225.11  section \<open>Sub-probability spaces\<close>
   226.1 --- a/src/HOL/Probability/Helly_Selection.thy	Fri Aug 18 14:57:23 2017 +0200
   226.2 +++ b/src/HOL/Probability/Helly_Selection.thy	Fri Aug 18 22:55:54 2017 +0200
   226.3 @@ -8,7 +8,7 @@
   226.4  text \<open>The set of bounded, monotone, right continuous functions is sequentially compact\<close>
   226.5  
   226.6  theory Helly_Selection
   226.7 -  imports "~~/src/HOL/Library/Diagonal_Subsequence" Weak_Convergence
   226.8 +  imports "HOL-Library.Diagonal_Subsequence" Weak_Convergence
   226.9  begin
  226.10  
  226.11  lemma minus_one_less: "x - 1 < (x::real)"
   227.1 --- a/src/HOL/Probability/PMF_Impl.thy	Fri Aug 18 14:57:23 2017 +0200
   227.2 +++ b/src/HOL/Probability/PMF_Impl.thy	Fri Aug 18 22:55:54 2017 +0200
   227.3 @@ -8,7 +8,7 @@
   227.4  section \<open>Code generation for PMFs\<close>
   227.5  
   227.6  theory PMF_Impl
   227.7 -imports Probability_Mass_Function "~~/src/HOL/Library/AList_Mapping"
   227.8 +imports Probability_Mass_Function "HOL-Library.AList_Mapping"
   227.9  begin
  227.10  
  227.11  subsection \<open>General code generation setup\<close>
   228.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Fri Aug 18 14:57:23 2017 +0200
   228.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Fri Aug 18 22:55:54 2017 +0200
   228.3 @@ -8,7 +8,7 @@
   228.4  theory Probability_Mass_Function
   228.5  imports
   228.6    Giry_Monad
   228.7 -  "~~/src/HOL/Library/Multiset"
   228.8 +  "HOL-Library.Multiset"
   228.9  begin
  228.10  
  228.11  lemma AE_emeasure_singleton:
   229.1 --- a/src/HOL/Probability/Probability_Measure.thy	Fri Aug 18 14:57:23 2017 +0200
   229.2 +++ b/src/HOL/Probability/Probability_Measure.thy	Fri Aug 18 22:55:54 2017 +0200
   229.3 @@ -6,7 +6,7 @@
   229.4  section \<open>Probability measure\<close>
   229.5  
   229.6  theory Probability_Measure
   229.7 -  imports "~~/src/HOL/Analysis/Analysis"
   229.8 +  imports "HOL-Analysis.Analysis"
   229.9  begin
  229.10  
  229.11  locale prob_space = finite_measure +
   230.1 --- a/src/HOL/Probability/Projective_Limit.thy	Fri Aug 18 14:57:23 2017 +0200
   230.2 +++ b/src/HOL/Probability/Projective_Limit.thy	Fri Aug 18 22:55:54 2017 +0200
   230.3 @@ -8,7 +8,7 @@
   230.4  imports
   230.5    Fin_Map
   230.6    Infinite_Product_Measure
   230.7 -  "~~/src/HOL/Library/Diagonal_Subsequence"
   230.8 +  "HOL-Library.Diagonal_Subsequence"
   230.9  begin
  230.10  
  230.11  subsection \<open>Sequences of Finite Maps in Compact Sets\<close>
   231.1 --- a/src/HOL/Probability/Random_Permutations.thy	Fri Aug 18 14:57:23 2017 +0200
   231.2 +++ b/src/HOL/Probability/Random_Permutations.thy	Fri Aug 18 22:55:54 2017 +0200
   231.3 @@ -13,7 +13,7 @@
   231.4  theory Random_Permutations
   231.5  imports 
   231.6    "~~/src/HOL/Probability/Probability_Mass_Function" 
   231.7 -  "~~/src/HOL/Library/Multiset_Permutations"
   231.8 +  "HOL-Library.Multiset_Permutations"
   231.9  begin
  231.10  
  231.11  text \<open>
   232.1 --- a/src/HOL/Probability/SPMF.thy	Fri Aug 18 14:57:23 2017 +0200
   232.2 +++ b/src/HOL/Probability/SPMF.thy	Fri Aug 18 22:55:54 2017 +0200
   232.3 @@ -4,8 +4,8 @@
   232.4  
   232.5  theory SPMF imports
   232.6    Probability_Mass_Function
   232.7 -  "~~/src/HOL/Library/Complete_Partial_Order2"
   232.8 -  "~~/src/HOL/Library/Rewrite"
   232.9 +  "HOL-Library.Complete_Partial_Order2"
  232.10 +  "HOL-Library.Rewrite"
  232.11  begin
  232.12  
  232.13  subsection \<open>Auxiliary material\<close>
   233.1 --- a/src/HOL/Probability/Stopping_Time.thy	Fri Aug 18 14:57:23 2017 +0200
   233.2 +++ b/src/HOL/Probability/Stopping_Time.thy	Fri Aug 18 22:55:54 2017 +0200
   233.3 @@ -3,7 +3,7 @@
   233.4  section {* Stopping times *}
   233.5  
   233.6  theory Stopping_Time
   233.7 -  imports "../Analysis/Analysis"
   233.8 +  imports "HOL-Analysis.Analysis"
   233.9  begin
  233.10  
  233.11  subsection \<open>Stopping Time\<close>
   234.1 --- a/src/HOL/Probability/Stream_Space.thy	Fri Aug 18 14:57:23 2017 +0200
   234.2 +++ b/src/HOL/Probability/Stream_Space.thy	Fri Aug 18 22:55:54 2017 +0200
   234.3 @@ -4,8 +4,8 @@
   234.4  theory Stream_Space
   234.5  imports
   234.6    Infinite_Product_Measure
   234.7 -  "~~/src/HOL/Library/Stream"
   234.8 -  "~~/src/HOL/Library/Linear_Temporal_Logic_on_Streams"
   234.9 +  "HOL-Library.Stream"
  234.10 +  "HOL-Library.Linear_Temporal_Logic_on_Streams"
  234.11  begin
  234.12  
  234.13  lemma stream_eq_Stream_iff: "s = x ## t \<longleftrightarrow> (shd s = x \<and> stl s = t)"
   235.1 --- a/src/HOL/Probability/Tree_Space.thy	Fri Aug 18 14:57:23 2017 +0200
   235.2 +++ b/src/HOL/Probability/Tree_Space.thy	Fri Aug 18 22:55:54 2017 +0200
   235.3 @@ -2,7 +2,7 @@
   235.4      Author:     Johannes Hölzl, CMU *)
   235.5  
   235.6  theory Tree_Space
   235.7 -  imports Analysis "~~/src/HOL/Library/Tree"
   235.8 +  imports "HOL-Analysis.Analysis" "HOL-Library.Tree"
   235.9  begin
  235.10  
  235.11  lemma countable_lfp:
   236.1 --- a/src/HOL/Probability/ex/Dining_Cryptographers.thy	Fri Aug 18 14:57:23 2017 +0200
   236.2 +++ b/src/HOL/Probability/ex/Dining_Cryptographers.thy	Fri Aug 18 22:55:54 2017 +0200
   236.3 @@ -1,5 +1,5 @@
   236.4  theory Dining_Cryptographers
   236.5 -imports "~~/src/HOL/Probability/Information"
   236.6 +imports "HOL-Probability.Information"
   236.7  begin
   236.8  
   236.9  lemma image_ex1_eq: "inj_on f A \<Longrightarrow> (b \<in> f ` A) \<longleftrightarrow> (\<exists>!x \<in> A. b = f x)"
   237.1 --- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Fri Aug 18 14:57:23 2017 +0200
   237.2 +++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Fri Aug 18 22:55:54 2017 +0200
   237.3 @@ -3,7 +3,7 @@
   237.4  section \<open>Formalization of a Countermeasure by Koepf \& Duermuth 2009\<close>
   237.5  
   237.6  theory Koepf_Duermuth_Countermeasure
   237.7 -  imports "~~/src/HOL/Probability/Information" "~~/src/HOL/Library/Permutation"
   237.8 +  imports "HOL-Probability.Information" "HOL-Library.Permutation"
   237.9  begin
  237.10  
  237.11  lemma SIGMA_image_vimage:
   238.1 --- a/src/HOL/Probability/ex/Measure_Not_CCC.thy	Fri Aug 18 14:57:23 2017 +0200
   238.2 +++ b/src/HOL/Probability/ex/Measure_Not_CCC.thy	Fri Aug 18 22:55:54 2017 +0200
   238.3 @@ -3,7 +3,7 @@
   238.4  section \<open>The Category of Measurable Spaces is not Cartesian Closed\<close>
   238.5  
   238.6  theory Measure_Not_CCC
   238.7 -  imports "~~/src/HOL/Probability/Probability"
   238.8 +  imports Probability
   238.9  begin
  238.10  
  238.11  text \<open>
   239.1 --- a/src/HOL/Prolog/HOHH.thy	Fri Aug 18 14:57:23 2017 +0200
   239.2 +++ b/src/HOL/Prolog/HOHH.thy	Fri Aug 18 22:55:54 2017 +0200
   239.3 @@ -5,7 +5,7 @@
   239.4  section \<open>Higher-order hereditary Harrop formulas\<close>
   239.5  
   239.6  theory HOHH
   239.7 -imports HOL
   239.8 +imports HOL.HOL
   239.9  begin
  239.10  
  239.11  ML_file "prolog.ML"
   240.1 --- a/src/HOL/Proofs/Extraction/Euclid.thy	Fri Aug 18 14:57:23 2017 +0200
   240.2 +++ b/src/HOL/Proofs/Extraction/Euclid.thy	Fri Aug 18 22:55:54 2017 +0200
   240.3 @@ -8,10 +8,10 @@
   240.4  
   240.5  theory Euclid
   240.6  imports
   240.7 -  "~~/src/HOL/Computational_Algebra/Primes"
   240.8 +  "HOL-Computational_Algebra.Primes"
   240.9    Util
  240.10 -  Old_Datatype
  240.11 -  "~~/src/HOL/Library/Code_Target_Numeral"
  240.12 +  "HOL-Library.Old_Datatype"
  240.13 +  "HOL-Library.Code_Target_Numeral"
  240.14  begin
  240.15  
  240.16  text \<open>
   241.1 --- a/src/HOL/Proofs/Extraction/Higman_Extraction.thy	Fri Aug 18 14:57:23 2017 +0200
   241.2 +++ b/src/HOL/Proofs/Extraction/Higman_Extraction.thy	Fri Aug 18 22:55:54 2017 +0200
   241.3 @@ -6,7 +6,7 @@
   241.4  subsection \<open>Extracting the program\<close>
   241.5  
   241.6  theory Higman_Extraction
   241.7 -imports Higman Old_Datatype "~~/src/HOL/Library/Open_State_Syntax"
   241.8 +imports Higman "HOL-Library.Old_Datatype" "HOL-Library.Open_State_Syntax"
   241.9  begin
  241.10  
  241.11  declare R.induct [ind_realizer]
   242.1 --- a/src/HOL/Proofs/Extraction/Pigeonhole.thy	Fri Aug 18 14:57:23 2017 +0200
   242.2 +++ b/src/HOL/Proofs/Extraction/Pigeonhole.thy	Fri Aug 18 22:55:54 2017 +0200
   242.3 @@ -5,7 +5,7 @@
   242.4  section \<open>The pigeonhole principle\<close>
   242.5  
   242.6  theory Pigeonhole
   242.7 -imports Util Old_Datatype "~~/src/HOL/Library/Code_Target_Numeral"
   242.8 +imports Util "HOL-Library.Old_Datatype" "HOL-Library.Code_Target_Numeral"
   242.9  begin
  242.10  
  242.11  text \<open>
   243.1 --- a/src/HOL/Proofs/Extraction/QuotRem.thy	Fri Aug 18 14:57:23 2017 +0200
   243.2 +++ b/src/HOL/Proofs/Extraction/QuotRem.thy	Fri Aug 18 22:55:54 2017 +0200
   243.3 @@ -5,7 +5,7 @@
   243.4  section \<open>Quotient and remainder\<close>
   243.5  
   243.6  theory QuotRem
   243.7 -imports Old_Datatype Util
   243.8 +imports "HOL-Library.Old_Datatype" Util
   243.9  begin
  243.10  
  243.11  text \<open>Derivation of quotient and remainder using program extraction.\<close>
   244.1 --- a/src/HOL/Proofs/Extraction/Warshall.thy	Fri Aug 18 14:57:23 2017 +0200
   244.2 +++ b/src/HOL/Proofs/Extraction/Warshall.thy	Fri Aug 18 22:55:54 2017 +0200
   244.3 @@ -5,7 +5,7 @@
   244.4  section \<open>Warshall's algorithm\<close>
   244.5  
   244.6  theory Warshall
   244.7 -imports Old_Datatype
   244.8 +imports "HOL-Library.Old_Datatype"
   244.9  begin
  244.10  
  244.11  text \<open>
   245.1 --- a/src/HOL/Proofs/ex/XML_Data.thy	Fri Aug 18 14:57:23 2017 +0200
   245.2 +++ b/src/HOL/Proofs/ex/XML_Data.thy	Fri Aug 18 22:55:54 2017 +0200
   245.3 @@ -6,7 +6,7 @@
   245.4  *)
   245.5  
   245.6  theory XML_Data
   245.7 -  imports "~~/src/HOL/Isar_Examples/Drinker"
   245.8 +  imports "HOL-Isar_Examples.Drinker"
   245.9  begin
  245.10  
  245.11  subsection \<open>Export and re-import of global proof terms\<close>
   246.1 --- a/src/HOL/Quickcheck_Examples/Hotel_Example.thy	Fri Aug 18 14:57:23 2017 +0200
   246.2 +++ b/src/HOL/Quickcheck_Examples/Hotel_Example.thy	Fri Aug 18 22:55:54 2017 +0200
   246.3 @@ -1,5 +1,5 @@
   246.4  theory Hotel_Example
   246.5 -imports Main "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
   246.6 +imports Main "HOL-Library.Predicate_Compile_Quickcheck"
   246.7  begin
   246.8  
   246.9  datatype guest = Guest0 | Guest1
   247.1 --- a/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Fri Aug 18 14:57:23 2017 +0200
   247.2 +++ b/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Fri Aug 18 22:55:54 2017 +0200
   247.3 @@ -6,7 +6,7 @@
   247.4  section \<open>Examples for the 'quickcheck' command\<close>
   247.5  
   247.6  theory Quickcheck_Examples
   247.7 -imports Complex_Main "~~/src/HOL/Library/Dlist" "~~/src/HOL/Library/DAList_Multiset"
   247.8 +imports Complex_Main "HOL-Library.Dlist" "HOL-Library.DAList_Multiset"
   247.9  begin
  247.10  
  247.11  text \<open>
   248.1 --- a/src/HOL/Quotient_Examples/DList.thy	Fri Aug 18 14:57:23 2017 +0200
   248.2 +++ b/src/HOL/Quotient_Examples/DList.thy	Fri Aug 18 22:55:54 2017 +0200
   248.3 @@ -8,7 +8,7 @@
   248.4  section \<open>Lists with distinct elements\<close>
   248.5  
   248.6  theory DList
   248.7 -imports "~~/src/HOL/Library/Quotient_List"
   248.8 +imports "HOL-Library.Quotient_List"
   248.9  begin
  248.10  
  248.11  text \<open>Some facts about lists\<close>
   249.1 --- a/src/HOL/Quotient_Examples/Int_Pow.thy	Fri Aug 18 14:57:23 2017 +0200
   249.2 +++ b/src/HOL/Quotient_Examples/Int_Pow.thy	Fri Aug 18 22:55:54 2017 +0200
   249.3 @@ -4,7 +4,7 @@
   249.4  *)
   249.5  
   249.6  theory Int_Pow
   249.7 -imports Main "~~/src/HOL/Algebra/Group"
   249.8 +imports Main "HOL-Algebra.Group"
   249.9  begin
  249.10  
  249.11  (*
   250.1 --- a/src/HOL/Quotient_Examples/Lift_Fun.thy	Fri Aug 18 14:57:23 2017 +0200
   250.2 +++ b/src/HOL/Quotient_Examples/Lift_Fun.thy	Fri Aug 18 22:55:54 2017 +0200
   250.3 @@ -6,7 +6,7 @@
   250.4  
   250.5  
   250.6  theory Lift_Fun
   250.7 -imports Main "~~/src/HOL/Library/Quotient_Syntax"
   250.8 +imports Main "HOL-Library.Quotient_Syntax"
   250.9  begin
  250.10  
  250.11  text \<open>This file is meant as a test case. 
   251.1 --- a/src/HOL/Quotient_Examples/Quotient_FSet.thy	Fri Aug 18 14:57:23 2017 +0200
   251.2 +++ b/src/HOL/Quotient_Examples/Quotient_FSet.thy	Fri Aug 18 22:55:54 2017 +0200
   251.3 @@ -13,7 +13,7 @@
   251.4  *********************************************************************)
   251.5  
   251.6  theory Quotient_FSet
   251.7 -imports "~~/src/HOL/Library/Multiset" "~~/src/HOL/Library/Quotient_List"
   251.8 +imports "HOL-Library.Multiset" "HOL-Library.Quotient_List"
   251.9  begin
  251.10  
  251.11  text \<open>
   252.1 --- a/src/HOL/Quotient_Examples/Quotient_Int.thy	Fri Aug 18 14:57:23 2017 +0200
   252.2 +++ b/src/HOL/Quotient_Examples/Quotient_Int.thy	Fri Aug 18 22:55:54 2017 +0200
   252.3 @@ -7,7 +7,7 @@
   252.4  *)
   252.5  
   252.6  theory Quotient_Int
   252.7 -imports "~~/src/HOL/Library/Quotient_Product" Nat
   252.8 +imports "HOL-Library.Quotient_Product" HOL.Nat
   252.9  begin
  252.10  
  252.11  fun
   253.1 --- a/src/HOL/Quotient_Examples/Quotient_Message.thy	Fri Aug 18 14:57:23 2017 +0200
   253.2 +++ b/src/HOL/Quotient_Examples/Quotient_Message.thy	Fri Aug 18 22:55:54 2017 +0200
   253.3 @@ -5,7 +5,7 @@
   253.4  *)
   253.5  
   253.6  theory Quotient_Message
   253.7 -imports Main "~~/src/HOL/Library/Quotient_Syntax"
   253.8 +imports Main "HOL-Library.Quotient_Syntax"
   253.9  begin
  253.10  
  253.11  subsection\<open>Defining the Free Algebra\<close>
   254.1 --- a/src/HOL/Quotient_Examples/Quotient_Rat.thy	Fri Aug 18 14:57:23 2017 +0200
   254.2 +++ b/src/HOL/Quotient_Examples/Quotient_Rat.thy	Fri Aug 18 22:55:54 2017 +0200
   254.3 @@ -4,8 +4,8 @@
   254.4  Rational numbers defined with the quotient package, based on 'HOL/Rat.thy' by Makarius.
   254.5  *)
   254.6  
   254.7 -theory Quotient_Rat imports Archimedean_Field
   254.8 -  "~~/src/HOL/Library/Quotient_Product"
   254.9 +theory Quotient_Rat imports HOL.Archimedean_Field
  254.10 +  "HOL-Library.Quotient_Product"
  254.11  begin
  254.12  
  254.13  definition
   255.1 --- a/src/HOL/ROOT	Fri Aug 18 14:57:23 2017 +0200
   255.2 +++ b/src/HOL/ROOT	Fri Aug 18 22:55:54 2017 +0200
   255.3 @@ -122,7 +122,7 @@
   255.4      mutually recursive relations.
   255.5    *}
   255.6    theories [document = false]
   255.7 -    "~~/src/HOL/Library/Old_Datatype"
   255.8 +    "HOL-Library.Old_Datatype"
   255.9    theories [quick_and_dirty]
  255.10      Common_Patterns
  255.11    theories
  255.12 @@ -143,11 +143,11 @@
  255.13  session "HOL-IMP" (timing) in IMP = "HOL-Library" +
  255.14    options [document_variants = document]
  255.15    theories [document = false]
  255.16 -    "~~/src/HOL/Library/While_Combinator"
  255.17 -    "~~/src/HOL/Library/Char_ord"
  255.18 -    "~~/src/HOL/Library/List_lexord"
  255.19 -    "~~/src/HOL/Library/Quotient_List"
  255.20 -    "~~/src/HOL/Library/Extended"
  255.21 +    "HOL-Library.While_Combinator"
  255.22 +    "HOL-Library.Char_ord"
  255.23 +    "HOL-Library.List_lexord"
  255.24 +    "HOL-Library.Quotient_List"
  255.25 +    "HOL-Library.Extended"
  255.26    theories
  255.27      BExp
  255.28      ASM
  255.29 @@ -200,8 +200,8 @@
  255.30      "HOL-Number_Theory"
  255.31    theories [document = false]
  255.32      Less_False
  255.33 -    "~~/src/HOL/Library/Multiset"
  255.34 -    "~~/src/HOL/Number_Theory/Fib"
  255.35 +    "HOL-Library.Multiset"
  255.36 +    "HOL-Number_Theory.Fib"
  255.37    theories
  255.38      Balance
  255.39      Tree_Map
  255.40 @@ -228,10 +228,10 @@
  255.41    sessions
  255.42      "HOL-Algebra"
  255.43    theories [document = false]
  255.44 -    "~~/src/HOL/Library/FuncSet"
  255.45 -    "~~/src/HOL/Library/Multiset"
  255.46 -    "~~/src/HOL/Algebra/Ring"
  255.47 -    "~~/src/HOL/Algebra/FiniteProduct"
  255.48 +    "HOL-Library.FuncSet"
  255.49 +    "HOL-Library.Multiset"
  255.50 +    "HOL-Algebra.Ring"
  255.51 +    "HOL-Algebra.FiniteProduct"
  255.52    theories
  255.53      Number_Theory
  255.54    document_files
  255.55 @@ -322,9 +322,9 @@
  255.56    *}
  255.57    theories [document = false]
  255.58      (* Preliminaries from set and number theory *)
  255.59 -    "~~/src/HOL/Library/FuncSet"
  255.60 -    "~~/src/HOL/Computational_Algebra/Primes"
  255.61 -    "~~/src/HOL/Library/Permutation"
  255.62 +    "HOL-Library.FuncSet"
  255.63 +    "HOL-Computational_Algebra.Primes"
  255.64 +    "HOL-Library.Permutation"
  255.65    theories
  255.66      (* Orders and Lattices *)
  255.67      Galois_Connection    (* Knaster-Tarski theorem and Galois connections *)
  255.68 @@ -414,9 +414,9 @@
  255.69  session "HOL-Imperative_HOL" in Imperative_HOL = "HOL-Library" +
  255.70    options [print_mode = "iff,no_brackets"]
  255.71    theories [document = false]
  255.72 -    "~~/src/HOL/Library/Countable"
  255.73 -    "~~/src/HOL/Library/Monad_Syntax"
  255.74 -    "~~/src/HOL/Library/LaTeXsugar"
  255.75 +    "HOL-Library.Countable"
  255.76 +    "HOL-Library.Monad_Syntax"
  255.77 +    "HOL-Library.LaTeXsugar"
  255.78    theories Imperative_HOL_ex
  255.79    document_files "root.bib" "root.tex"
  255.80  
  255.81 @@ -446,10 +446,10 @@
  255.82      "HOL-Library"
  255.83      "HOL-Computational_Algebra"
  255.84    theories [document = false]
  255.85 -    "~~/src/HOL/Library/Code_Target_Numeral"
  255.86 -    "~~/src/HOL/Library/Monad_Syntax"
  255.87 -    "~~/src/HOL/Computational_Algebra/Primes"
  255.88 -    "~~/src/HOL/Library/Open_State_Syntax"
  255.89 +    "HOL-Library.Code_Target_Numeral"
  255.90 +    "HOL-Library.Monad_Syntax"
  255.91 +    "HOL-Computational_Algebra.Primes"
  255.92 +    "HOL-Library.Open_State_Syntax"
  255.93    theories
  255.94      Greatest_Common_Divisor
  255.95      Warshall
  255.96 @@ -501,7 +501,7 @@
  255.97    sessions
  255.98      "HOL-Eisbach"
  255.99    theories [document = false]
 255.100 -    "~~/src/HOL/Library/While_Combinator"
 255.101 +    "HOL-Library.While_Combinator"
 255.102    theories
 255.103      MicroJava
 255.104    document_files
 255.105 @@ -664,8 +664,8 @@
 255.106    *}
 255.107    options [quick_and_dirty]
 255.108    theories [document = false]
 255.109 -    "~~/src/HOL/Library/Lattice_Syntax"
 255.110 -    "../Computational_Algebra/Primes"
 255.111 +    "HOL-Library.Lattice_Syntax"
 255.112 +    "HOL-Computational_Algebra.Primes"
 255.113    theories
 255.114      Knaster_Tarski
 255.115      Peirce
 255.116 @@ -705,7 +705,7 @@
 255.117      Verification of the SET Protocol.
 255.118    *}
 255.119    theories [document = false]
 255.120 -    "~~/src/HOL/Library/Nat_Bijection"
 255.121 +    "HOL-Library.Nat_Bijection"
 255.122    theories
 255.123      SET_Protocol
 255.124    document_files "root.tex"
 255.125 @@ -756,11 +756,11 @@
 255.126  
 255.127  session "HOL-Probability" (main timing) in "Probability" = "HOL-Analysis" +
 255.128    theories [document = false]
 255.129 -    "~~/src/HOL/Library/Countable"
 255.130 -    "~~/src/HOL/Library/Permutation"
 255.131 -    "~~/src/HOL/Library/Order_Continuity"
 255.132 -    "~~/src/HOL/Library/Diagonal_Subsequence"
 255.133 -    "~~/src/HOL/Library/Finite_Map"
 255.134 +    "HOL-Library.Countable"
 255.135 +    "HOL-Library.Permutation"
 255.136 +    "HOL-Library.Order_Continuity"
 255.137 +    "HOL-Library.Diagonal_Subsequence"
 255.138 +    "HOL-Library.Finite_Map"
 255.139    theories
 255.140      Probability (global)
 255.141    document_files "root.tex"
 255.142 @@ -1084,8 +1084,8 @@
 255.143    sessions
 255.144      "HOL-Library"
 255.145    theories [document = false]
 255.146 -    "~~/src/HOL/Library/Nat_Bijection"
 255.147 -    "~~/src/HOL/Library/Countable"
 255.148 +    "HOL-Library.Nat_Bijection"
 255.149 +    "HOL-Library.Countable"
 255.150    theories
 255.151      HOLCF (global)
 255.152    document_files "root.tex"
   256.1 --- a/src/HOL/SET_Protocol/Message_SET.thy	Fri Aug 18 14:57:23 2017 +0200
   256.2 +++ b/src/HOL/SET_Protocol/Message_SET.thy	Fri Aug 18 22:55:54 2017 +0200
   256.3 @@ -7,7 +7,7 @@
   256.4  section\<open>The Message Theory, Modified for SET\<close>
   256.5  
   256.6  theory Message_SET
   256.7 -imports Main "~~/src/HOL/Library/Nat_Bijection"
   256.8 +imports Main "HOL-Library.Nat_Bijection"
   256.9  begin
  256.10  
  256.11  subsection\<open>General Lemmas\<close>
   257.1 --- a/src/HOL/SMT_Examples/SMT_Word_Examples.thy	Fri Aug 18 14:57:23 2017 +0200
   257.2 +++ b/src/HOL/SMT_Examples/SMT_Word_Examples.thy	Fri Aug 18 22:55:54 2017 +0200
   257.3 @@ -5,7 +5,7 @@
   257.4  section \<open>Word examples for for SMT binding\<close>
   257.5  
   257.6  theory SMT_Word_Examples
   257.7 -imports "~~/src/HOL/Word/Word"
   257.8 +imports "HOL-Word.Word"
   257.9  begin
  257.10  
  257.11  declare [[smt_oracle = true]]
   258.1 --- a/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy	Fri Aug 18 14:57:23 2017 +0200
   258.2 +++ b/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy	Fri Aug 18 22:55:54 2017 +0200
   258.3 @@ -4,7 +4,7 @@
   258.4  *)
   258.5  
   258.6  theory Greatest_Common_Divisor
   258.7 -imports "../../SPARK"
   258.8 +imports SPARK
   258.9  begin
  258.10  
  258.11  spark_proof_functions
   259.1 --- a/src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy	Fri Aug 18 14:57:23 2017 +0200
   259.2 +++ b/src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy	Fri Aug 18 22:55:54 2017 +0200
   259.3 @@ -4,7 +4,7 @@
   259.4  *)
   259.5  
   259.6  theory Longest_Increasing_Subsequence
   259.7 -imports "../../SPARK"
   259.8 +imports SPARK
   259.9  begin
  259.10  
  259.11  text \<open>
   260.1 --- a/src/HOL/SPARK/Examples/RIPEMD-160/RMD.thy	Fri Aug 18 14:57:23 2017 +0200
   260.2 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/RMD.thy	Fri Aug 18 22:55:54 2017 +0200
   260.3 @@ -5,7 +5,7 @@
   260.4  *)
   260.5  
   260.6  theory RMD
   260.7 -imports "~~/src/HOL/Word/Word"
   260.8 +imports "HOL-Word.Word"
   260.9  begin
  260.10  
  260.11  
   261.1 --- a/src/HOL/SPARK/Examples/RIPEMD-160/RMD_Specification.thy	Fri Aug 18 14:57:23 2017 +0200
   261.2 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/RMD_Specification.thy	Fri Aug 18 22:55:54 2017 +0200
   261.3 @@ -5,7 +5,7 @@
   261.4  *)
   261.5  
   261.6  theory RMD_Specification
   261.7 -imports RMD "~~/src/HOL/SPARK/SPARK"
   261.8 +imports RMD SPARK
   261.9  begin
  261.10  
  261.11  (* bit operations *)
   262.1 --- a/src/HOL/SPARK/Examples/Sqrt/Sqrt.thy	Fri Aug 18 14:57:23 2017 +0200
   262.2 +++ b/src/HOL/SPARK/Examples/Sqrt/Sqrt.thy	Fri Aug 18 22:55:54 2017 +0200
   262.3 @@ -4,7 +4,7 @@
   262.4  *)
   262.5  
   262.6  theory Sqrt
   262.7 -imports "../../SPARK"
   262.8 +imports SPARK
   262.9  begin
  262.10  
  262.11  spark_open "sqrt/isqrt"
   263.1 --- a/src/HOL/SPARK/Manual/Complex_Types.thy	Fri Aug 18 14:57:23 2017 +0200
   263.2 +++ b/src/HOL/SPARK/Manual/Complex_Types.thy	Fri Aug 18 22:55:54 2017 +0200
   263.3 @@ -1,5 +1,5 @@
   263.4  theory Complex_Types
   263.5 -imports "../SPARK"
   263.6 +imports SPARK
   263.7  begin
   263.8  
   263.9  datatype day = Mon | Tue | Wed | Thu | Fri | Sat | Sun
   264.1 --- a/src/HOL/SPARK/Manual/Example_Verification.thy	Fri Aug 18 14:57:23 2017 +0200
   264.2 +++ b/src/HOL/SPARK/Manual/Example_Verification.thy	Fri Aug 18 22:55:54 2017 +0200
   264.3 @@ -1,6 +1,6 @@
   264.4  (*<*)
   264.5  theory Example_Verification
   264.6 -imports "../Examples/Gcd/Greatest_Common_Divisor" Simple_Greatest_Common_Divisor
   264.7 +imports "HOL-SPARK-Examples.Greatest_Common_Divisor" Simple_Greatest_Common_Divisor
   264.8  begin
   264.9  (*>*)
  264.10  
   265.1 --- a/src/HOL/SPARK/Manual/Proc1.thy	Fri Aug 18 14:57:23 2017 +0200
   265.2 +++ b/src/HOL/SPARK/Manual/Proc1.thy	Fri Aug 18 22:55:54 2017 +0200
   265.3 @@ -1,5 +1,5 @@
   265.4  theory Proc1
   265.5 -imports "../SPARK"
   265.6 +imports SPARK
   265.7  begin
   265.8  
   265.9  spark_open "loop_invariant/proc1"
   266.1 --- a/src/HOL/SPARK/Manual/Proc2.thy	Fri Aug 18 14:57:23 2017 +0200
   266.2 +++ b/src/HOL/SPARK/Manual/Proc2.thy	Fri Aug 18 22:55:54 2017 +0200
   266.3 @@ -1,5 +1,5 @@
   266.4  theory Proc2
   266.5 -imports "../SPARK"
   266.6 +imports SPARK
   266.7  begin
   266.8  
   266.9  spark_open "loop_invariant/proc2"
   267.1 --- a/src/HOL/SPARK/Manual/Reference.thy	Fri Aug 18 14:57:23 2017 +0200
   267.2 +++ b/src/HOL/SPARK/Manual/Reference.thy	Fri Aug 18 22:55:54 2017 +0200
   267.3 @@ -1,6 +1,6 @@
   267.4  (*<*)
   267.5  theory Reference
   267.6 -imports "../SPARK"
   267.7 +imports SPARK
   267.8  begin
   267.9  
  267.10  syntax (my_constrain output)
   268.1 --- a/src/HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy	Fri Aug 18 14:57:23 2017 +0200
   268.2 +++ b/src/HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy	Fri Aug 18 22:55:54 2017 +0200
   268.3 @@ -4,7 +4,7 @@
   268.4  *)
   268.5  
   268.6  theory Simple_Greatest_Common_Divisor
   268.7 -imports "../SPARK"
   268.8 +imports SPARK
   268.9  begin
  268.10  
  268.11  spark_proof_functions
   269.1 --- a/src/HOL/SPARK/SPARK_Setup.thy	Fri Aug 18 14:57:23 2017 +0200
   269.2 +++ b/src/HOL/SPARK/SPARK_Setup.thy	Fri Aug 18 22:55:54 2017 +0200
   269.3 @@ -6,7 +6,7 @@
   269.4  *)
   269.5  
   269.6  theory SPARK_Setup
   269.7 -imports "~~/src/HOL/Word/Word" "~~/src/HOL/Word/Bit_Comparison"
   269.8 +imports "HOL-Word.Word" "HOL-Word.Bit_Comparison"
   269.9  keywords
  269.10    "spark_open_vcg" :: thy_load ("vcg", "fdl", "rls") and
  269.11    "spark_open" :: thy_load ("siv", "fdl", "rls") and
   270.1 --- a/src/HOL/TLA/Buffer/Buffer.thy	Fri Aug 18 14:57:23 2017 +0200
   270.2 +++ b/src/HOL/TLA/Buffer/Buffer.thy	Fri Aug 18 22:55:54 2017 +0200
   270.3 @@ -5,7 +5,7 @@
   270.4  section \<open>A simple FIFO buffer (synchronous communication, interleaving)\<close>
   270.5  
   270.6  theory Buffer
   270.7 -imports "../TLA"
   270.8 +imports "HOL-TLA.TLA"
   270.9  begin
  270.10  
  270.11  (* actions *)
   271.1 --- a/src/HOL/TLA/Inc/Inc.thy	Fri Aug 18 14:57:23 2017 +0200
   271.2 +++ b/src/HOL/TLA/Inc/Inc.thy	Fri Aug 18 22:55:54 2017 +0200
   271.3 @@ -5,7 +5,7 @@
   271.4  section \<open>Lamport's "increment" example\<close>
   271.5  
   271.6  theory Inc
   271.7 -imports "../TLA"
   271.8 +imports "HOL-TLA.TLA"
   271.9  begin
  271.10  
  271.11  (* program counter as an enumeration type *)
   272.1 --- a/src/HOL/TLA/Memory/ProcedureInterface.thy	Fri Aug 18 14:57:23 2017 +0200
   272.2 +++ b/src/HOL/TLA/Memory/ProcedureInterface.thy	Fri Aug 18 22:55:54 2017 +0200
   272.3 @@ -5,7 +5,7 @@
   272.4  section \<open>Procedure interface for RPC-Memory components\<close>
   272.5  
   272.6  theory ProcedureInterface
   272.7 -imports "../TLA" RPCMemoryParams
   272.8 +imports "HOL-TLA.TLA" RPCMemoryParams
   272.9  begin
  272.10  
  272.11  typedecl ('a,'r) chan
   273.1 --- a/src/HOL/TPTP/ATP_Problem_Import.thy	Fri Aug 18 14:57:23 2017 +0200
   273.2 +++ b/src/HOL/TPTP/ATP_Problem_Import.thy	Fri Aug 18 22:55:54 2017 +0200
   273.3 @@ -5,7 +5,7 @@
   273.4  section \<open>ATP Problem Importer\<close>
   273.5  
   273.6  theory ATP_Problem_Import
   273.7 -imports Complex_Main TPTP_Interpret "~~/src/HOL/Library/Refute"
   273.8 +imports Complex_Main TPTP_Interpret "HOL-Library.Refute"
   273.9  begin
  273.10  
  273.11  ML_file "sledgehammer_tactics.ML"
   274.1 --- a/src/HOL/UNITY/Comp/AllocBase.thy	Fri Aug 18 14:57:23 2017 +0200
   274.2 +++ b/src/HOL/UNITY/Comp/AllocBase.thy	Fri Aug 18 22:55:54 2017 +0200
   274.3 @@ -5,7 +5,7 @@
   274.4  
   274.5  section\<open>Common Declarations for Chandy and Charpentier's Allocator\<close>
   274.6  
   274.7 -theory AllocBase imports "../UNITY_Main" "~~/src/HOL/Library/Multiset_Order" begin
   274.8 +theory AllocBase imports "../UNITY_Main" "HOL-Library.Multiset_Order" begin
   274.9  
  274.10  consts Nclients :: nat  (*Number of clients*)
  274.11  
   275.1 --- a/src/HOL/UNITY/Follows.thy	Fri Aug 18 14:57:23 2017 +0200
   275.2 +++ b/src/HOL/UNITY/Follows.thy	Fri Aug 18 22:55:54 2017 +0200
   275.3 @@ -6,7 +6,7 @@
   275.4  section\<open>The Follows Relation of Charpentier and Sivilotte\<close>
   275.5  
   275.6  theory Follows
   275.7 -imports SubstAx ListOrder "~~/src/HOL/Library/Multiset"
   275.8 +imports SubstAx ListOrder "HOL-Library.Multiset"
   275.9  begin
  275.10  
  275.11  definition Follows :: "['a => 'b::{order}, 'a => 'b::{order}] => 'a program set" (infixl "Fols" 65) where
   276.1 --- a/src/HOL/UNITY/Simple/NSP_Bad.thy	Fri Aug 18 14:57:23 2017 +0200
   276.2 +++ b/src/HOL/UNITY/Simple/NSP_Bad.thy	Fri Aug 18 22:55:54 2017 +0200
   276.3 @@ -7,7 +7,7 @@
   276.4  
   276.5  section\<open>Analyzing the Needham-Schroeder Public-Key Protocol in UNITY\<close>
   276.6  
   276.7 -theory NSP_Bad imports "../../Auth/Public" "../UNITY_Main" begin
   276.8 +theory NSP_Bad imports "HOL-Auth.Public" "../UNITY_Main" begin
   276.9  
  276.10  text\<open>This is the flawed version, vulnerable to Lowe's attack.
  276.11  From page 260 of
   277.1 --- a/src/HOL/Unix/Unix.thy	Fri Aug 18 14:57:23 2017 +0200
   277.2 +++ b/src/HOL/Unix/Unix.thy	Fri Aug 18 22:55:54 2017 +0200
   277.3 @@ -7,7 +7,7 @@
   277.4  theory Unix
   277.5    imports
   277.6      Nested_Environment
   277.7 -    "~~/src/HOL/Library/Sublist"
   277.8 +    "HOL-Library.Sublist"
   277.9  begin
  277.10  
  277.11  text \<open>
   278.1 --- a/src/HOL/Word/Bits_Bit.thy	Fri Aug 18 14:57:23 2017 +0200
   278.2 +++ b/src/HOL/Word/Bits_Bit.thy	Fri Aug 18 22:55:54 2017 +0200
   278.3 @@ -5,7 +5,7 @@
   278.4  section \<open>Bit operations in $\cal Z_2$\<close>
   278.5  
   278.6  theory Bits_Bit
   278.7 -imports Bits "~~/src/HOL/Library/Bit"
   278.8 +imports Bits "HOL-Library.Bit"
   278.9  begin
  278.10  
  278.11  instantiation bit :: bit
   279.1 --- a/src/HOL/Word/Examples/WordExamples.thy	Fri Aug 18 14:57:23 2017 +0200
   279.2 +++ b/src/HOL/Word/Examples/WordExamples.thy	Fri Aug 18 22:55:54 2017 +0200
   279.3 @@ -7,7 +7,7 @@
   279.4  section "Examples of word operations"
   279.5  
   279.6  theory WordExamples
   279.7 -  imports "../Word" "../WordBitwise"
   279.8 +  imports "HOL-Word.Word" "HOL-Word.WordBitwise"
   279.9  begin
  279.10  
  279.11  type_synonym word32 = "32 word"
   280.1 --- a/src/HOL/Word/Word.thy	Fri Aug 18 14:57:23 2017 +0200
   280.2 +++ b/src/HOL/Word/Word.thy	Fri Aug 18 22:55:54 2017 +0200
   280.3 @@ -6,8 +6,8 @@
   280.4  
   280.5  theory Word
   280.6  imports
   280.7 -  "~~/src/HOL/Library/Type_Length"
   280.8 -  "~~/src/HOL/Library/Boolean_Algebra"
   280.9 +  "HOL-Library.Type_Length"
  280.10 +  "HOL-Library.Boolean_Algebra"
  280.11    Bits_Bit
  280.12    Bool_List_Representation
  280.13    Misc_Typedef
   281.1 --- a/src/HOL/Word/Word_Miscellaneous.thy	Fri Aug 18 14:57:23 2017 +0200
   281.2 +++ b/src/HOL/Word/Word_Miscellaneous.thy	Fri Aug 18 22:55:54 2017 +0200
   281.3 @@ -3,7 +3,7 @@
   281.4  section \<open>Miscellaneous lemmas, of at least doubtful value\<close>
   281.5  
   281.6  theory Word_Miscellaneous
   281.7 -  imports "~~/src/HOL/Library/Bit" Misc_Numeric
   281.8 +  imports "HOL-Library.Bit" Misc_Numeric
   281.9  begin
  281.10  
  281.11  lemma power_minus_simp: "0 < n \<Longrightarrow> a ^ n = a * a ^ (n - 1)"
   282.1 --- a/src/HOL/ZF/LProd.thy	Fri Aug 18 14:57:23 2017 +0200
   282.2 +++ b/src/HOL/ZF/LProd.thy	Fri Aug 18 22:55:54 2017 +0200
   282.3 @@ -6,7 +6,7 @@
   282.4  *)
   282.5  
   282.6  theory LProd 
   282.7 -imports "~~/src/HOL/Library/Multiset"
   282.8 +imports "HOL-Library.Multiset"
   282.9  begin
  282.10  
  282.11  inductive_set
   283.1 --- a/src/HOL/ex/Adhoc_Overloading_Examples.thy	Fri Aug 18 14:57:23 2017 +0200
   283.2 +++ b/src/HOL/ex/Adhoc_Overloading_Examples.thy	Fri Aug 18 22:55:54 2017 +0200
   283.3 @@ -7,8 +7,8 @@
   283.4  theory Adhoc_Overloading_Examples
   283.5  imports
   283.6    Main
   283.7 -  "~~/src/HOL/Library/Infinite_Set"
   283.8 -  "~~/src/Tools/Adhoc_Overloading"
   283.9 +  "HOL-Library.Infinite_Set"
  283.10 +  "HOL-Library.Adhoc_Overloading"
  283.11  begin
  283.12  
  283.13  text \<open>Adhoc overloading allows to overload a constant depending on
   284.1 --- a/src/HOL/ex/Ballot.thy	Fri Aug 18 14:57:23 2017 +0200
   284.2 +++ b/src/HOL/ex/Ballot.thy	Fri Aug 18 22:55:54 2017 +0200
   284.3 @@ -8,7 +8,7 @@
   284.4  theory Ballot
   284.5  imports
   284.6    Complex_Main
   284.7 -  "~~/src/HOL/Library/FuncSet"
   284.8 +  "HOL-Library.FuncSet"
   284.9  begin
  284.10  
  284.11  subsection \<open>Preliminaries\<close>
   285.1 --- a/src/HOL/ex/Birthday_Paradox.thy	Fri Aug 18 14:57:23 2017 +0200
   285.2 +++ b/src/HOL/ex/Birthday_Paradox.thy	Fri Aug 18 22:55:54 2017 +0200
   285.3 @@ -5,7 +5,7 @@
   285.4  section \<open>A Formulation of the Birthday Paradox\<close>
   285.5  
   285.6  theory Birthday_Paradox
   285.7 -imports Main "~~/src/HOL/Binomial" "~~/src/HOL/Library/FuncSet"
   285.8 +imports Main HOL.Binomial "HOL-Library.FuncSet"
   285.9  begin
  285.10  
  285.11  section \<open>Cardinality\<close>
   286.1 --- a/src/HOL/ex/Bubblesort.thy	Fri Aug 18 14:57:23 2017 +0200
   286.2 +++ b/src/HOL/ex/Bubblesort.thy	Fri Aug 18 22:55:54 2017 +0200
   286.3 @@ -3,7 +3,7 @@
   286.4  section \<open>Bubblesort\<close>
   286.5  
   286.6  theory Bubblesort
   286.7 -imports "~~/src/HOL/Library/Multiset"
   286.8 +imports "HOL-Library.Multiset"
   286.9  begin
  286.10  
  286.11  text\<open>This is \emph{a} version of bubblesort.\<close>
   287.1 --- a/src/HOL/ex/Code_Binary_Nat_examples.thy	Fri Aug 18 14:57:23 2017 +0200
   287.2 +++ b/src/HOL/ex/Code_Binary_Nat_examples.thy	Fri Aug 18 22:55:54 2017 +0200
   287.3 @@ -5,7 +5,7 @@
   287.4  section \<open>Simple examples for natural numbers implemented in binary representation.\<close>
   287.5  
   287.6  theory Code_Binary_Nat_examples
   287.7 -imports Complex_Main "~~/src/HOL/Library/Code_Binary_Nat"
   287.8 +imports Complex_Main "HOL-Library.Code_Binary_Nat"
   287.9  begin
  287.10  
  287.11  fun to_n :: "nat \<Rightarrow> nat list"
   288.1 --- a/src/HOL/ex/Code_Timing.thy	Fri Aug 18 14:57:23 2017 +0200
   288.2 +++ b/src/HOL/ex/Code_Timing.thy	Fri Aug 18 22:55:54 2017 +0200
   288.3 @@ -5,7 +5,7 @@
   288.4  section \<open>Examples for code generation timing measures\<close>
   288.5  
   288.6  theory Code_Timing
   288.7 -imports "~~/src/HOL/Number_Theory/Eratosthenes"
   288.8 +imports "HOL-Number_Theory.Eratosthenes"
   288.9  begin
  288.10  
  288.11  declare [[code_timing]]
   289.1 --- a/src/HOL/ex/Computations.thy	Fri Aug 18 14:57:23 2017 +0200
   289.2 +++ b/src/HOL/ex/Computations.thy	Fri Aug 18 22:55:54 2017 +0200
   289.3 @@ -5,7 +5,7 @@
   289.4  section \<open>Simple example for computations generated by the code generator\<close>
   289.5  
   289.6  theory Computations
   289.7 -  imports "../Nat" "../Fun_Def" "../Num" "../Code_Numeral"
   289.8 +  imports HOL.Nat HOL.Fun_Def HOL.Num HOL.Code_Numeral
   289.9  begin
  289.10  
  289.11  fun even :: "nat \<Rightarrow> bool"
   290.1 --- a/src/HOL/ex/Execute_Choice.thy	Fri Aug 18 14:57:23 2017 +0200
   290.2 +++ b/src/HOL/ex/Execute_Choice.thy	Fri Aug 18 22:55:54 2017 +0200
   290.3 @@ -3,7 +3,7 @@
   290.4  section \<open>A simple cookbook example how to eliminate choice in programs.\<close>
   290.5  
   290.6  theory Execute_Choice
   290.7 -imports Main "~~/src/HOL/Library/AList_Mapping"
   290.8 +imports Main "HOL-Library.AList_Mapping"
   290.9  begin
  290.10  
  290.11  text \<open>
   291.1 --- a/src/HOL/ex/Functions.thy	Fri Aug 18 14:57:23 2017 +0200
   291.2 +++ b/src/HOL/ex/Functions.thy	Fri Aug 18 22:55:54 2017 +0200
   291.3 @@ -5,7 +5,7 @@
   291.4  section \<open>Examples of function definitions\<close>
   291.5  
   291.6  theory Functions
   291.7 -imports Main "~~/src/HOL/Library/Monad_Syntax"
   291.8 +imports Main "HOL-Library.Monad_Syntax"
   291.9  begin
  291.10  
  291.11  subsection \<open>Very basic\<close>
   292.1 --- a/src/HOL/ex/Groebner_Examples.thy	Fri Aug 18 14:57:23 2017 +0200
   292.2 +++ b/src/HOL/ex/Groebner_Examples.thy	Fri Aug 18 22:55:54 2017 +0200
   292.3 @@ -5,7 +5,7 @@
   292.4  section \<open>Groebner Basis Examples\<close>
   292.5  
   292.6  theory Groebner_Examples
   292.7 -imports "~~/src/HOL/Groebner_Basis"
   292.8 +imports HOL.Groebner_Basis
   292.9  begin
  292.10  
  292.11  subsection \<open>Basic examples\<close>
   293.1 --- a/src/HOL/ex/IArray_Examples.thy	Fri Aug 18 14:57:23 2017 +0200
   293.2 +++ b/src/HOL/ex/IArray_Examples.thy	Fri Aug 18 22:55:54 2017 +0200
   293.3 @@ -1,5 +1,5 @@
   293.4  theory IArray_Examples
   293.5 -imports "~~/src/HOL/Library/IArray" "~~/src/HOL/Library/Code_Target_Numeral"
   293.6 +imports "HOL-Library.IArray" "HOL-Library.Code_Target_Numeral"
   293.7  begin
   293.8  
   293.9  lemma "IArray [True,False] !! 1 = False"
   294.1 --- a/src/HOL/ex/MergeSort.thy	Fri Aug 18 14:57:23 2017 +0200
   294.2 +++ b/src/HOL/ex/MergeSort.thy	Fri Aug 18 22:55:54 2017 +0200
   294.3 @@ -6,7 +6,7 @@
   294.4  section\<open>Merge Sort\<close>
   294.5  
   294.6  theory MergeSort
   294.7 -imports "~~/src/HOL/Library/Multiset"
   294.8 +imports "HOL-Library.Multiset"
   294.9  begin
  294.10  
  294.11  context linorder
   295.1 --- a/src/HOL/ex/Parallel_Example.thy	Fri Aug 18 14:57:23 2017 +0200
   295.2 +++ b/src/HOL/ex/Parallel_Example.thy	Fri Aug 18 22:55:54 2017 +0200
   295.3 @@ -1,7 +1,7 @@
   295.4  section \<open>A simple example demonstrating parallelism for code generated towards Isabelle/ML\<close>
   295.5  
   295.6  theory Parallel_Example
   295.7 -imports Complex_Main "~~/src/HOL/Library/Parallel" "~~/src/HOL/Library/Debug"
   295.8 +imports Complex_Main "HOL-Library.Parallel" "HOL-Library.Debug"
   295.9  begin
  295.10  
  295.11  subsection \<open>Compute-intensive examples.\<close>
   296.1 --- a/src/HOL/ex/Perm_Fragments.thy	Fri Aug 18 14:57:23 2017 +0200
   296.2 +++ b/src/HOL/ex/Perm_Fragments.thy	Fri Aug 18 22:55:54 2017 +0200
   296.3 @@ -3,7 +3,7 @@
   296.4  section \<open>Fragments on permuations\<close>
   296.5  
   296.6  theory Perm_Fragments
   296.7 -imports "~~/src/HOL/Library/Perm" "~~/src/HOL/Library/Dlist"
   296.8 +imports "HOL-Library.Perm" "HOL-Library.Dlist"
   296.9  begin
  296.10  
  296.11  unbundle permutation_syntax
   297.1 --- a/src/HOL/ex/PresburgerEx.thy	Fri Aug 18 14:57:23 2017 +0200
   297.2 +++ b/src/HOL/ex/PresburgerEx.thy	Fri Aug 18 22:55:54 2017 +0200
   297.3 @@ -5,7 +5,7 @@
   297.4  section \<open>Some examples for Presburger Arithmetic\<close>
   297.5  
   297.6  theory PresburgerEx
   297.7 -imports Presburger
   297.8 +imports HOL.Presburger
   297.9  begin
  297.10  
  297.11  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
   298.1 --- a/src/HOL/ex/Quicksort.thy	Fri Aug 18 14:57:23 2017 +0200
   298.2 +++ b/src/HOL/ex/Quicksort.thy	Fri Aug 18 22:55:54 2017 +0200
   298.3 @@ -5,7 +5,7 @@
   298.4  section \<open>Quicksort with function package\<close>
   298.5  
   298.6  theory Quicksort
   298.7 -imports "~~/src/HOL/Library/Multiset"
   298.8 +imports "HOL-Library.Multiset"
   298.9  begin
  298.10  
  298.11  context linorder
   299.1 --- a/src/HOL/ex/Reflection_Examples.thy	Fri Aug 18 14:57:23 2017 +0200
   299.2 +++ b/src/HOL/ex/Reflection_Examples.thy	Fri Aug 18 22:55:54 2017 +0200
   299.3 @@ -5,7 +5,7 @@
   299.4  section \<open>Examples for generic reflection and reification\<close>
   299.5  
   299.6  theory Reflection_Examples
   299.7 -imports Complex_Main "~~/src/HOL/Library/Reflection"
   299.8 +imports Complex_Main "HOL-Library.Reflection"
   299.9  begin
  299.10  
  299.11  text \<open>This theory presents two methods: reify and reflection\<close>
   300.1 --- a/src/HOL/ex/Refute_Examples.thy	Fri Aug 18 14:57:23 2017 +0200
   300.2 +++ b/src/HOL/ex/Refute_Examples.thy	Fri Aug 18 22:55:54 2017 +0200
   300.3 @@ -8,7 +8,7 @@
   300.4  section \<open>Examples for the 'refute' command\<close>
   300.5  
   300.6  theory Refute_Examples
   300.7 -imports "~~/src/HOL/Library/Refute"
   300.8 +imports "HOL-Library.Refute"
   300.9  begin
  300.10  
  300.11  refute_params [satsolver = "cdclite"]
   301.1 --- a/src/HOL/ex/Rewrite_Examples.thy	Fri Aug 18 14:57:23 2017 +0200
   301.2 +++ b/src/HOL/ex/Rewrite_Examples.thy	Fri Aug 18 22:55:54 2017 +0200
   301.3 @@ -1,5 +1,5 @@
   301.4  theory Rewrite_Examples
   301.5 -imports Main "~~/src/HOL/Library/Rewrite"
   301.6 +imports Main "HOL-Library.Rewrite"
   301.7  begin
   301.8  
   301.9  section \<open>The rewrite Proof Method by Example\<close>
   302.1 --- a/src/HOL/ex/SOS.thy	Fri Aug 18 14:57:23 2017 +0200
   302.2 +++ b/src/HOL/ex/SOS.thy	Fri Aug 18 22:55:54 2017 +0200
   302.3 @@ -6,7 +6,7 @@
   302.4  *)
   302.5  
   302.6  theory SOS
   302.7 -imports "~~/src/HOL/Library/Sum_of_Squares"
   302.8 +imports "HOL-Library.Sum_of_Squares"
   302.9  begin
  302.10  
  302.11  lemma "(3::real) * x + 7 * a < 4 & 3 < 2 * x \<Longrightarrow> a < 0"
   303.1 --- a/src/HOL/ex/SOS_Cert.thy	Fri Aug 18 14:57:23 2017 +0200
   303.2 +++ b/src/HOL/ex/SOS_Cert.thy	Fri Aug 18 22:55:54 2017 +0200
   303.3 @@ -6,7 +6,7 @@
   303.4  *)
   303.5  
   303.6  theory SOS_Cert
   303.7 -imports "~~/src/HOL/Library/Sum_of_Squares"
   303.8 +imports "HOL-Library.Sum_of_Squares"
   303.9  begin
  303.10  
  303.11  lemma "(3::real) * x + 7 * a < 4 \<and> 3 < 2 * x \<Longrightarrow> a < 0"
   304.1 --- a/src/HOL/ex/Simps_Case_Conv_Examples.thy	Fri Aug 18 14:57:23 2017 +0200
   304.2 +++ b/src/HOL/ex/Simps_Case_Conv_Examples.thy	Fri Aug 18 22:55:54 2017 +0200
   304.3 @@ -1,5 +1,5 @@
   304.4  theory Simps_Case_Conv_Examples imports
   304.5 -  "~~/src/HOL/Library/Simps_Case_Conv"
   304.6 +  "HOL-Library.Simps_Case_Conv"
   304.7  begin
   304.8  
   304.9  section \<open>Tests for the Simps<->Case conversion tools\<close>
   305.1 --- a/src/HOL/ex/Sqrt.thy	Fri Aug 18 14:57:23 2017 +0200
   305.2 +++ b/src/HOL/ex/Sqrt.thy	Fri Aug 18 22:55:54 2017 +0200
   305.3 @@ -5,7 +5,7 @@
   305.4  section \<open>Square roots of primes are irrational\<close>
   305.5  
   305.6  theory Sqrt
   305.7 -imports Complex_Main "~~/src/HOL/Computational_Algebra/Primes"
   305.8 +imports Complex_Main "HOL-Computational_Algebra.Primes"
   305.9  begin
  305.10  
  305.11  text \<open>The square root of any prime number (including 2) is irrational.\<close>
   306.1 --- a/src/HOL/ex/Sqrt_Script.thy	Fri Aug 18 14:57:23 2017 +0200
   306.2 +++ b/src/HOL/ex/Sqrt_Script.thy	Fri Aug 18 22:55:54 2017 +0200
   306.3 @@ -6,7 +6,7 @@
   306.4  section \<open>Square roots of primes are irrational (script version)\<close>
   306.5  
   306.6  theory Sqrt_Script
   306.7 -imports Complex_Main "~~/src/HOL/Computational_Algebra/Primes"
   306.8 +imports Complex_Main "HOL-Computational_Algebra.Primes"
   306.9  begin
  306.10  
  306.11  text \<open>
   307.1 --- a/src/HOL/ex/Tarski.thy	Fri Aug 18 14:57:23 2017 +0200
   307.2 +++ b/src/HOL/ex/Tarski.thy	Fri Aug 18 22:55:54 2017 +0200
   307.3 @@ -5,7 +5,7 @@
   307.4  section \<open>The Full Theorem of Tarski\<close>
   307.5  
   307.6  theory Tarski
   307.7 -imports Main "~~/src/HOL/Library/FuncSet"
   307.8 +imports Main "HOL-Library.FuncSet"
   307.9  begin
  307.10  
  307.11  text \<open>
   308.1 --- a/src/HOL/ex/Termination.thy	Fri Aug 18 14:57:23 2017 +0200
   308.2 +++ b/src/HOL/ex/Termination.thy	Fri Aug 18 22:55:54 2017 +0200
   308.3 @@ -6,7 +6,7 @@
   308.4  section \<open>Examples and regression tests for automated termination proofs\<close>
   308.5   
   308.6  theory Termination
   308.7 -imports Main "~~/src/HOL/Library/Multiset"
   308.8 +imports Main "HOL-Library.Multiset"
   308.9  begin
  308.10  
  308.11  subsection \<open>Manually giving termination relations using \<open>relation\<close> and
   309.1 --- a/src/HOL/ex/ThreeDivides.thy	Fri Aug 18 14:57:23 2017 +0200
   309.2 +++ b/src/HOL/ex/ThreeDivides.thy	Fri Aug 18 22:55:54 2017 +0200
   309.3 @@ -5,7 +5,7 @@
   309.4  section \<open>Three Divides Theorem\<close>
   309.5  
   309.6  theory ThreeDivides
   309.7 -imports Main "~~/src/HOL/Library/LaTeXsugar"
   309.8 +imports Main "HOL-Library.LaTeXsugar"
   309.9  begin
  309.10  
  309.11  subsection \<open>Abstract\<close>
   310.1 --- a/src/HOL/ex/Transfer_Debug.thy	Fri Aug 18 14:57:23 2017 +0200
   310.2 +++ b/src/HOL/ex/Transfer_Debug.thy	Fri Aug 18 22:55:54 2017 +0200
   310.3 @@ -2,7 +2,7 @@
   310.4      Author:     Ondřej Kunčar, TU München
   310.5  *)
   310.6  theory Transfer_Debug 
   310.7 -imports Main "~~/src/HOL/Library/FSet"
   310.8 +imports Main "HOL-Library.FSet"
   310.9  begin                              
  310.10  
  310.11  (*
   311.1 --- a/src/HOL/ex/Transitive_Closure_Table_Ex.thy	Fri Aug 18 14:57:23 2017 +0200
   311.2 +++ b/src/HOL/ex/Transitive_Closure_Table_Ex.thy	Fri Aug 18 22:55:54 2017 +0200
   311.3 @@ -3,7 +3,7 @@
   311.4  section \<open>Simple example for table-based implementation of the reflexive transitive closure\<close>
   311.5  
   311.6  theory Transitive_Closure_Table_Ex
   311.7 -imports "~~/src/HOL/Library/Transitive_Closure_Table"
   311.8 +imports "HOL-Library.Transitive_Closure_Table"
   311.9  begin
  311.10  
  311.11  datatype ty = A | B | C
   312.1 --- a/src/HOL/ex/While_Combinator_Example.thy	Fri Aug 18 14:57:23 2017 +0200
   312.2 +++ b/src/HOL/ex/While_Combinator_Example.thy	Fri Aug 18 22:55:54 2017 +0200
   312.3 @@ -6,7 +6,7 @@
   312.4  section \<open>An application of the While combinator\<close>
   312.5  
   312.6  theory While_Combinator_Example
   312.7 -imports "~~/src/HOL/Library/While_Combinator"
   312.8 +imports "HOL-Library.While_Combinator"
   312.9  begin
  312.10  
  312.11  text \<open>Computation of the @{term lfp} on finite sets via 
   313.1 --- a/src/HOL/ex/Word_Type.thy	Fri Aug 18 14:57:23 2017 +0200
   313.2 +++ b/src/HOL/ex/Word_Type.thy	Fri Aug 18 22:55:54 2017 +0200
   313.3 @@ -6,7 +6,7 @@
   313.4  theory Word_Type
   313.5    imports
   313.6      Main
   313.7 -    "~~/src/HOL/Library/Type_Length"
   313.8 +    "HOL-Library.Type_Length"
   313.9  begin
  313.10  
  313.11  subsection \<open>Truncating bit representations of numeric types\<close>
   314.1 --- a/src/LCF/LCF.thy	Fri Aug 18 14:57:23 2017 +0200
   314.2 +++ b/src/LCF/LCF.thy	Fri Aug 18 22:55:54 2017 +0200
   314.3 @@ -6,7 +6,7 @@
   314.4  section \<open>LCF on top of First-Order Logic\<close>
   314.5  
   314.6  theory LCF
   314.7 -imports "~~/src/FOL/FOL"
   314.8 +imports FOL
   314.9  begin
  314.10  
  314.11  text \<open>This theory is based on Lawrence Paulson's book Logic and Computation.\<close>
   315.1 --- a/src/Pure/context.ML	Fri Aug 18 14:57:23 2017 +0200
   315.2 +++ b/src/Pure/context.ML	Fri Aug 18 22:55:54 2017 +0200
   315.3 @@ -165,9 +165,7 @@
   315.4  val finished = ~1;
   315.5  
   315.6  fun display_name thy_id =
   315.7 -  let
   315.8 -    val {name = long_name, stage} = history_of_id thy_id;
   315.9 -    val name = Long_Name.base_name long_name;
  315.10 +  let val {name, stage} = history_of_id thy_id;
  315.11    in if stage = finished then name else name ^ ":" ^ string_of_int stage end;
  315.12  
  315.13  fun display_names thy =
   316.1 --- a/src/ZF/UNITY/MultisetSum.thy	Fri Aug 18 14:57:23 2017 +0200
   316.2 +++ b/src/ZF/UNITY/MultisetSum.thy	Fri Aug 18 22:55:54 2017 +0200
   316.3 @@ -5,7 +5,7 @@
   316.4  section \<open>Setsum for Multisets\<close>
   316.5  
   316.6  theory MultisetSum
   316.7 -imports "../Induct/Multiset"
   316.8 +imports "ZF-Induct.Multiset"
   316.9  begin
  316.10  
  316.11  definition
   317.1 --- a/src/ZF/ZF_Base.thy	Fri Aug 18 14:57:23 2017 +0200
   317.2 +++ b/src/ZF/ZF_Base.thy	Fri Aug 18 22:55:54 2017 +0200
   317.3 @@ -6,7 +6,7 @@
   317.4  section \<open>Base of Zermelo-Fraenkel Set Theory\<close>
   317.5  
   317.6  theory ZF_Base
   317.7 -imports "~~/src/FOL/FOL"
   317.8 +imports FOL
   317.9  begin
  317.10  
  317.11  subsection \<open>Signature\<close>