explicit file specifications -- avoid secondary load path;
authorwenzelm
Wed Dec 29 17:34:41 2010 +0100 (2010-12-29)
changeset 4141364cd30d6b0b8
parent 41412 35f30e07fe0d
child 41414 00b2b6716ed8
explicit file specifications -- avoid secondary load path;
doc-src/Classes/Thy/Setup.thy
doc-src/LaTeXsugar/Sugar/ROOT.ML
doc-src/LaTeXsugar/Sugar/Sugar.thy
doc-src/TutorialI/Sets/Examples.thy
src/HOL/Algebra/Divisibility.thy
src/HOL/Algebra/Exponent.thy
src/HOL/Algebra/Group.thy
src/HOL/Algebra/ROOT.ML
src/HOL/Auth/Guard/Guard_Shared.thy
src/HOL/Auth/ROOT.ML
src/HOL/Auth/Smartcard/Smartcard.thy
src/HOL/Auth/TLS.thy
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Decision_Procs/Cooper.thy
src/HOL/Decision_Procs/Ferrack.thy
src/HOL/Decision_Procs/MIR.thy
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
src/HOL/HOLCF/Bifinite.thy
src/HOL/HOLCF/FOCUS/Fstream.thy
src/HOL/HOLCF/FOCUS/Fstreams.thy
src/HOL/HOLCF/FOCUS/Stream_adm.thy
src/HOL/HOLCF/Library/Stream.thy
src/HOL/HOLCF/ROOT.ML
src/HOL/HOLCF/Universal.thy
src/HOL/HOLCF/ex/Dagstuhl.thy
src/HOL/HOLCF/ex/Focus_ex.thy
src/HOL/Hahn_Banach/Bounds.thy
src/HOL/Hahn_Banach/Vector_Space.thy
src/HOL/Imperative_HOL/Heap.thy
src/HOL/Imperative_HOL/Heap_Monad.thy
src/HOL/Imperative_HOL/Overview.thy
src/HOL/Imperative_HOL/ROOT.ML
src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
src/HOL/Imperative_HOL/ex/SatChecker.thy
src/HOL/Imperative_HOL/ex/Sublist.thy
src/HOL/Import/HOL4Compat.thy
src/HOL/IsaMakefile
src/HOL/Isar_Examples/Knaster_Tarski.thy
src/HOL/Matrix/ComputeFloat.thy
src/HOL/Matrix/LP.thy
src/HOL/Matrix/Matrix.thy
src/HOL/Metis_Examples/Abstraction.thy
src/HOL/Metis_Examples/BigO.thy
src/HOL/Metis_Examples/Tarski.thy
src/HOL/MicroJava/BV/BVExample.thy
src/HOL/MicroJava/DFA/Kildall.thy
src/HOL/MicroJava/DFA/Semilat.thy
src/HOL/MicroJava/ROOT.ML
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/NSA/NSComplex.thy
src/HOL/Nitpick_Examples/Manual_Nits.thy
src/HOL/Nominal/Nominal.thy
src/HOL/Nominal/ROOT.ML
src/HOL/Number_Theory/UniqueFactorization.thy
src/HOL/Old_Number_Theory/Factorization.thy
src/HOL/Old_Number_Theory/Finite2.thy
src/HOL/Old_Number_Theory/ROOT.ML
src/HOL/Predicate_Compile_Examples/Examples.thy
src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy
src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy
src/HOL/Predicate_Compile_Examples/IMP_1.thy
src/HOL/Predicate_Compile_Examples/IMP_2.thy
src/HOL/Predicate_Compile_Examples/IMP_3.thy
src/HOL/Predicate_Compile_Examples/IMP_4.thy
src/HOL/Predicate_Compile_Examples/List_Examples.thy
src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy
src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy
src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy
src/HOL/Probability/Information.thy
src/HOL/Probability/Positive_Extended_Real.thy
src/HOL/Probability/Sigma_Algebra.thy
src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy
src/HOL/Proofs/Extraction/Euclid.thy
src/HOL/Proofs/Extraction/Higman.thy
src/HOL/Proofs/Extraction/Pigeonhole.thy
src/HOL/Proofs/Extraction/ROOT.ML
src/HOL/Proofs/Lambda/ROOT.ML
src/HOL/Proofs/Lambda/WeakNorm.thy
src/HOL/Quotient_Examples/FSet.thy
src/HOL/Quotient_Examples/Quotient_Int.thy
src/HOL/SET_Protocol/Message_SET.thy
src/HOL/SET_Protocol/ROOT.ML
src/HOL/UNITY/Follows.thy
src/HOL/Unix/Unix.thy
src/HOL/Word/Bit_Operations.thy
src/HOL/Word/Bit_Representation.thy
src/HOL/Word/Type_Length.thy
src/HOL/Word/Word.thy
src/HOL/ZF/LProd.thy
src/HOL/ex/Efficient_Nat_examples.thy
src/HOL/ex/Execute_Choice.thy
src/HOL/ex/Fundefs.thy
src/HOL/ex/Landau.thy
src/HOL/ex/MergeSort.thy
src/HOL/ex/Quickcheck_Lattice_Examples.thy
src/HOL/ex/Quicksort.thy
src/HOL/ex/ROOT.ML
src/HOL/ex/ReflectionEx.thy
src/HOL/ex/Sorting.thy
src/HOL/ex/Tarski.thy
src/HOL/ex/Termination.thy
src/HOL/ex/ThreeDivides.thy
src/HOL/ex/While_Combinator_Example.thy
     1.1 --- a/doc-src/Classes/Thy/Setup.thy	Wed Dec 29 13:51:17 2010 +0100
     1.2 +++ b/doc-src/Classes/Thy/Setup.thy	Wed Dec 29 17:34:41 2010 +0100
     1.3 @@ -1,5 +1,5 @@
     1.4  theory Setup
     1.5 -imports Main Code_Integer
     1.6 +imports Main "~~/src/HOL/Library/Code_Integer"
     1.7  uses
     1.8    "../../antiquote_setup.ML"
     1.9    "../../more_antiquote.ML"
     2.1 --- a/doc-src/LaTeXsugar/Sugar/ROOT.ML	Wed Dec 29 13:51:17 2010 +0100
     2.2 +++ b/doc-src/LaTeXsugar/Sugar/ROOT.ML	Wed Dec 29 17:34:41 2010 +0100
     2.3 @@ -1,4 +1,6 @@
     2.4 -no_document use_thy "LaTeXsugar";
     2.5 -no_document use_thy "OptionalSugar";
     2.6 +no_document use_thys [
     2.7 +  "~~/src/HOL/Library/LaTeXsugar",
     2.8 +  "~~/src/HOL/Library/OptionalSugar"
     2.9 +];
    2.10  use_thy "Sugar";
    2.11  
     3.1 --- a/doc-src/LaTeXsugar/Sugar/Sugar.thy	Wed Dec 29 13:51:17 2010 +0100
     3.2 +++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy	Wed Dec 29 17:34:41 2010 +0100
     3.3 @@ -1,6 +1,6 @@
     3.4  (*<*)
     3.5  theory Sugar
     3.6 -imports LaTeXsugar OptionalSugar
     3.7 +imports "~~/src/HOL/Library/LaTeXsugar" "~~/src/HOL/Library/OptionalSugar"
     3.8  begin
     3.9  (*>*)
    3.10  
     4.1 --- a/doc-src/TutorialI/Sets/Examples.thy	Wed Dec 29 13:51:17 2010 +0100
     4.2 +++ b/doc-src/TutorialI/Sets/Examples.thy	Wed Dec 29 17:34:41 2010 +0100
     4.3 @@ -1,4 +1,4 @@
     4.4 -theory Examples imports Main Binomial begin
     4.5 +theory Examples imports Main "~~/src/HOL/Library/Binomial" begin
     4.6  
     4.7  declare [[eta_contract = false]]
     4.8  ML "Pretty.margin_default := 64"
     5.1 --- a/src/HOL/Algebra/Divisibility.thy	Wed Dec 29 13:51:17 2010 +0100
     5.2 +++ b/src/HOL/Algebra/Divisibility.thy	Wed Dec 29 17:34:41 2010 +0100
     5.3 @@ -5,7 +5,7 @@
     5.4  *)
     5.5  
     5.6  theory Divisibility
     5.7 -imports Permutation Coset Group
     5.8 +imports "~~/src/HOL/Library/Permutation" Coset Group
     5.9  begin
    5.10  
    5.11  section {* Factorial Monoids *}
     6.1 --- a/src/HOL/Algebra/Exponent.thy	Wed Dec 29 13:51:17 2010 +0100
     6.2 +++ b/src/HOL/Algebra/Exponent.thy	Wed Dec 29 17:34:41 2010 +0100
     6.3 @@ -6,7 +6,7 @@
     6.4  *)
     6.5  
     6.6  theory Exponent
     6.7 -imports Main "~~/src/HOL/Old_Number_Theory/Primes" Binomial
     6.8 +imports Main "~~/src/HOL/Old_Number_Theory/Primes" "~~/src/HOL/Library/Binomial"
     6.9  begin
    6.10  
    6.11  section {*Sylow's Theorem*}
     7.1 --- a/src/HOL/Algebra/Group.thy	Wed Dec 29 13:51:17 2010 +0100
     7.2 +++ b/src/HOL/Algebra/Group.thy	Wed Dec 29 17:34:41 2010 +0100
     7.3 @@ -5,7 +5,7 @@
     7.4  *)
     7.5  
     7.6  theory Group
     7.7 -imports Lattice FuncSet
     7.8 +imports Lattice "~~/src/HOL/Library/FuncSet"
     7.9  begin
    7.10  
    7.11  section {* Monoids and Groups *}
     8.1 --- a/src/HOL/Algebra/ROOT.ML	Wed Dec 29 13:51:17 2010 +0100
     8.2 +++ b/src/HOL/Algebra/ROOT.ML	Wed Dec 29 17:34:41 2010 +0100
     8.3 @@ -4,7 +4,12 @@
     8.4  *)
     8.5  
     8.6  (* Preliminaries from set and number theory *)
     8.7 -no_document use_thys ["FuncSet", "~~/src/HOL/Old_Number_Theory/Primes", "Binomial", "Permutation"];
     8.8 +no_document use_thys [
     8.9 +  "~~/src/HOL/Library/FuncSet",
    8.10 +  "~~/src/HOL/Old_Number_Theory/Primes",
    8.11 +  "~~/src/HOL/Library/Binomial",
    8.12 +  "~~/src/HOL/Library/Permutation"
    8.13 +];
    8.14  
    8.15  
    8.16  (*** New development, based on explicit structures ***)
     9.1 --- a/src/HOL/Auth/Guard/Guard_Shared.thy	Wed Dec 29 13:51:17 2010 +0100
     9.2 +++ b/src/HOL/Auth/Guard/Guard_Shared.thy	Wed Dec 29 17:34:41 2010 +0100
     9.3 @@ -11,7 +11,7 @@
     9.4  
     9.5  header{*lemmas on guarded messages for protocols with symmetric keys*}
     9.6  
     9.7 -theory Guard_Shared imports Guard GuardK Shared begin
     9.8 +theory Guard_Shared imports Guard GuardK "../Shared" begin
     9.9  
    9.10  subsection{*Extensions to Theory @{text Shared}*}
    9.11  
    10.1 --- a/src/HOL/Auth/ROOT.ML	Wed Dec 29 13:51:17 2010 +0100
    10.2 +++ b/src/HOL/Auth/ROOT.ML	Wed Dec 29 17:34:41 2010 +0100
    10.3 @@ -1,2 +1,7 @@
    10.4 -
    10.5 -use_thys ["Auth_Shared", "Auth_Public", "Smartcard/Auth_Smartcard", "Guard/Auth_Guard_Shared", "Guard/Auth_Guard_Public"];
    10.6 +use_thys [
    10.7 +  "Auth_Shared",
    10.8 +  "Auth_Public",
    10.9 +  "Smartcard/Auth_Smartcard",
   10.10 +  "Guard/Auth_Guard_Shared",
   10.11 +  "Guard/Auth_Guard_Public"
   10.12 +];
    11.1 --- a/src/HOL/Auth/Smartcard/Smartcard.thy	Wed Dec 29 13:51:17 2010 +0100
    11.2 +++ b/src/HOL/Auth/Smartcard/Smartcard.thy	Wed Dec 29 17:34:41 2010 +0100
    11.3 @@ -4,7 +4,7 @@
    11.4  header{*Theory of smartcards*}
    11.5  
    11.6  theory Smartcard
    11.7 -imports EventSC All_Symmetric
    11.8 +imports EventSC "../All_Symmetric"
    11.9  begin
   11.10  
   11.11  text{*  
    12.1 --- a/src/HOL/Auth/TLS.thy	Wed Dec 29 13:51:17 2010 +0100
    12.2 +++ b/src/HOL/Auth/TLS.thy	Wed Dec 29 17:34:41 2010 +0100
    12.3 @@ -40,7 +40,7 @@
    12.4  
    12.5  header{*The TLS Protocol: Transport Layer Security*}
    12.6  
    12.7 -theory TLS imports Public Nat_Bijection begin
    12.8 +theory TLS imports Public "~~/src/HOL/Library/Nat_Bijection" begin
    12.9  
   12.10  definition certificate :: "[agent,key] => msg" where
   12.11      "certificate A KA == Crypt (priSK Server) {|Agent A, Key KA|}"
    13.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Wed Dec 29 13:51:17 2010 +0100
    13.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Wed Dec 29 17:34:41 2010 +0100
    13.3 @@ -4,7 +4,12 @@
    13.4  header {* Prove Real Valued Inequalities by Computation *}
    13.5  
    13.6  theory Approximation
    13.7 -imports Complex_Main Float Reflection "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Efficient_Nat
    13.8 +imports
    13.9 +  Complex_Main
   13.10 +  "~~/src/HOL/Library/Float"
   13.11 +  "~~/src/HOL/Library/Reflection"
   13.12 +  "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
   13.13 +  "~~/src/HOL/Library/Efficient_Nat"
   13.14  begin
   13.15  
   13.16  section "Horner Scheme"
    14.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Wed Dec 29 13:51:17 2010 +0100
    14.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Wed Dec 29 17:34:41 2010 +0100
    14.3 @@ -3,7 +3,7 @@
    14.4  *)
    14.5  
    14.6  theory Cooper
    14.7 -imports Complex_Main Efficient_Nat
    14.8 +imports Complex_Main "~~/src/HOL/Library/Efficient_Nat"
    14.9  uses ("cooper_tac.ML")
   14.10  begin
   14.11  
    15.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Wed Dec 29 13:51:17 2010 +0100
    15.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Wed Dec 29 17:34:41 2010 +0100
    15.3 @@ -3,7 +3,7 @@
    15.4  *)
    15.5  
    15.6  theory Ferrack
    15.7 -imports Complex_Main Dense_Linear_Order Efficient_Nat
    15.8 +imports Complex_Main Dense_Linear_Order "~~/src/HOL/Library/Efficient_Nat"
    15.9  uses ("ferrack_tac.ML")
   15.10  begin
   15.11  
    16.1 --- a/src/HOL/Decision_Procs/MIR.thy	Wed Dec 29 13:51:17 2010 +0100
    16.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Wed Dec 29 17:34:41 2010 +0100
    16.3 @@ -3,7 +3,7 @@
    16.4  *)
    16.5  
    16.6  theory MIR
    16.7 -imports Complex_Main Dense_Linear_Order Efficient_Nat
    16.8 +imports Complex_Main Dense_Linear_Order "~~/src/HOL/Library/Efficient_Nat"
    16.9  uses ("mir_tac.ML")
   16.10  begin
   16.11  
    17.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Dec 29 13:51:17 2010 +0100
    17.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Dec 29 17:34:41 2010 +0100
    17.3 @@ -5,9 +5,10 @@
    17.4  header{* A formalization of Ferrante and Rackoff's procedure with polynomial parameters, see Paper in CALCULEMUS 2008 *}
    17.5  
    17.6  theory Parametric_Ferrante_Rackoff
    17.7 -imports Reflected_Multivariate_Polynomial
    17.8 +imports
    17.9 +  Reflected_Multivariate_Polynomial
   17.10    Dense_Linear_Order
   17.11 -  Efficient_Nat
   17.12 +  "~~/src/HOL/Library/Efficient_Nat"
   17.13  begin
   17.14  
   17.15  subsection {* Terms *}
    18.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Wed Dec 29 13:51:17 2010 +0100
    18.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Wed Dec 29 17:34:41 2010 +0100
    18.3 @@ -5,7 +5,7 @@
    18.4  header {* Implementation and verification of multivariate polynomials *}
    18.5  
    18.6  theory Reflected_Multivariate_Polynomial
    18.7 -imports Complex_Main Abstract_Rat Polynomial_List
    18.8 +imports Complex_Main "~~/src/HOL/Library/Abstract_Rat" Polynomial_List
    18.9  begin
   18.10  
   18.11    (* Implementation *)
    19.1 --- a/src/HOL/HOLCF/Bifinite.thy	Wed Dec 29 13:51:17 2010 +0100
    19.2 +++ b/src/HOL/HOLCF/Bifinite.thy	Wed Dec 29 17:34:41 2010 +0100
    19.3 @@ -5,7 +5,7 @@
    19.4  header {* Profinite and bifinite cpos *}
    19.5  
    19.6  theory Bifinite
    19.7 -imports Map_Functions Countable
    19.8 +imports Map_Functions "~~/src/HOL/Library/Countable"
    19.9  begin
   19.10  
   19.11  default_sort cpo
    20.1 --- a/src/HOL/HOLCF/FOCUS/Fstream.thy	Wed Dec 29 13:51:17 2010 +0100
    20.2 +++ b/src/HOL/HOLCF/FOCUS/Fstream.thy	Wed Dec 29 17:34:41 2010 +0100
    20.3 @@ -9,7 +9,7 @@
    20.4  header {* FOCUS flat streams *}
    20.5  
    20.6  theory Fstream
    20.7 -imports Stream
    20.8 +imports "~~/src/HOL/HOLCF/Library/Stream"
    20.9  begin
   20.10  
   20.11  default_sort type
    21.1 --- a/src/HOL/HOLCF/FOCUS/Fstreams.thy	Wed Dec 29 13:51:17 2010 +0100
    21.2 +++ b/src/HOL/HOLCF/FOCUS/Fstreams.thy	Wed Dec 29 17:34:41 2010 +0100
    21.3 @@ -7,7 +7,7 @@
    21.4  *)
    21.5  
    21.6  theory Fstreams
    21.7 -imports Stream
    21.8 +imports "~~/src/HOL/HOLCF/Library/Stream"
    21.9  begin
   21.10  
   21.11  default_sort type
    22.1 --- a/src/HOL/HOLCF/FOCUS/Stream_adm.thy	Wed Dec 29 13:51:17 2010 +0100
    22.2 +++ b/src/HOL/HOLCF/FOCUS/Stream_adm.thy	Wed Dec 29 17:34:41 2010 +0100
    22.3 @@ -5,7 +5,7 @@
    22.4  header {* Admissibility for streams *}
    22.5  
    22.6  theory Stream_adm
    22.7 -imports Stream Continuity
    22.8 +imports "~~/src/HOL/HOLCF/Library/Stream" "~~/src/HOL/Library/Continuity"
    22.9  begin
   22.10  
   22.11  definition
    23.1 --- a/src/HOL/HOLCF/Library/Stream.thy	Wed Dec 29 13:51:17 2010 +0100
    23.2 +++ b/src/HOL/HOLCF/Library/Stream.thy	Wed Dec 29 17:34:41 2010 +0100
    23.3 @@ -5,7 +5,7 @@
    23.4  header {* General Stream domain *}
    23.5  
    23.6  theory Stream
    23.7 -imports HOLCF Nat_Infinity
    23.8 +imports HOLCF "~~/src/HOL/Library/Nat_Infinity"
    23.9  begin
   23.10  
   23.11  default_sort pcpo
    24.1 --- a/src/HOL/HOLCF/ROOT.ML	Wed Dec 29 13:51:17 2010 +0100
    24.2 +++ b/src/HOL/HOLCF/ROOT.ML	Wed Dec 29 17:34:41 2010 +0100
    24.3 @@ -4,6 +4,6 @@
    24.4  HOLCF -- a semantic extension of HOL by the LCF logic.
    24.5  *)
    24.6  
    24.7 -no_document use_thys ["Nat_Bijection", "Countable"];
    24.8 +no_document use_thys ["~~/src/HOL/Library/Nat_Bijection", "~~/src/HOL/Library/Countable"];
    24.9  
   24.10  use_thys ["Plain_HOLCF", "Fixrec", "HOLCF"];
    25.1 --- a/src/HOL/HOLCF/Universal.thy	Wed Dec 29 13:51:17 2010 +0100
    25.2 +++ b/src/HOL/HOLCF/Universal.thy	Wed Dec 29 17:34:41 2010 +0100
    25.3 @@ -5,7 +5,7 @@
    25.4  header {* A universal bifinite domain *}
    25.5  
    25.6  theory Universal
    25.7 -imports Bifinite Completion Nat_Bijection
    25.8 +imports Bifinite Completion "~~/src/HOL/Library/Nat_Bijection"
    25.9  begin
   25.10  
   25.11  subsection {* Basis for universal domain *}
    26.1 --- a/src/HOL/HOLCF/ex/Dagstuhl.thy	Wed Dec 29 13:51:17 2010 +0100
    26.2 +++ b/src/HOL/HOLCF/ex/Dagstuhl.thy	Wed Dec 29 17:34:41 2010 +0100
    26.3 @@ -1,5 +1,5 @@
    26.4  theory Dagstuhl
    26.5 -imports Stream
    26.6 +imports "~~/src/HOL/HOLCF/Library/Stream"
    26.7  begin
    26.8  
    26.9  axiomatization
    27.1 --- a/src/HOL/HOLCF/ex/Focus_ex.thy	Wed Dec 29 13:51:17 2010 +0100
    27.2 +++ b/src/HOL/HOLCF/ex/Focus_ex.thy	Wed Dec 29 17:34:41 2010 +0100
    27.3 @@ -99,7 +99,7 @@
    27.4  *)
    27.5  
    27.6  theory Focus_ex
    27.7 -imports Stream
    27.8 +imports "~~/src/HOL/HOLCF/Library/Stream"
    27.9  begin
   27.10  
   27.11  typedecl ('a, 'b) tc
    28.1 --- a/src/HOL/Hahn_Banach/Bounds.thy	Wed Dec 29 13:51:17 2010 +0100
    28.2 +++ b/src/HOL/Hahn_Banach/Bounds.thy	Wed Dec 29 17:34:41 2010 +0100
    28.3 @@ -5,7 +5,7 @@
    28.4  header {* Bounds *}
    28.5  
    28.6  theory Bounds
    28.7 -imports Main ContNotDenum
    28.8 +imports Main "~~/src/HOL/Library/ContNotDenum"
    28.9  begin
   28.10  
   28.11  locale lub =
    29.1 --- a/src/HOL/Hahn_Banach/Vector_Space.thy	Wed Dec 29 13:51:17 2010 +0100
    29.2 +++ b/src/HOL/Hahn_Banach/Vector_Space.thy	Wed Dec 29 17:34:41 2010 +0100
    29.3 @@ -5,7 +5,7 @@
    29.4  header {* Vector spaces *}
    29.5  
    29.6  theory Vector_Space
    29.7 -imports Real Bounds Zorn
    29.8 +imports Real Bounds "~~/src/HOL/Library/Zorn"
    29.9  begin
   29.10  
   29.11  subsection {* Signature *}
    30.1 --- a/src/HOL/Imperative_HOL/Heap.thy	Wed Dec 29 13:51:17 2010 +0100
    30.2 +++ b/src/HOL/Imperative_HOL/Heap.thy	Wed Dec 29 17:34:41 2010 +0100
    30.3 @@ -5,7 +5,7 @@
    30.4  header {* A polymorphic heap based on cantor encodings *}
    30.5  
    30.6  theory Heap
    30.7 -imports Main Countable
    30.8 +imports Main "~~/src/HOL/Library/Countable"
    30.9  begin
   30.10  
   30.11  subsection {* Representable types *}
    31.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Wed Dec 29 13:51:17 2010 +0100
    31.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Wed Dec 29 17:34:41 2010 +0100
    31.3 @@ -5,7 +5,10 @@
    31.4  header {* A monad with a polymorphic heap and primitive reasoning infrastructure *}
    31.5  
    31.6  theory Heap_Monad
    31.7 -imports Heap Monad_Syntax Code_Natural
    31.8 +imports
    31.9 +  Heap
   31.10 +  "~~/src/HOL/Library/Monad_Syntax"
   31.11 +  "~~/src/HOL/Library/Code_Natural"
   31.12  begin
   31.13  
   31.14  subsection {* The monad *}
    32.1 --- a/src/HOL/Imperative_HOL/Overview.thy	Wed Dec 29 13:51:17 2010 +0100
    32.2 +++ b/src/HOL/Imperative_HOL/Overview.thy	Wed Dec 29 17:34:41 2010 +0100
    32.3 @@ -4,7 +4,7 @@
    32.4  
    32.5  (*<*)
    32.6  theory Overview
    32.7 -imports Imperative_HOL LaTeXsugar
    32.8 +imports Imperative_HOL "~~/src/HOL/Library/LaTeXsugar"
    32.9  begin
   32.10  
   32.11  (* type constraints with spacing *)
    33.1 --- a/src/HOL/Imperative_HOL/ROOT.ML	Wed Dec 29 13:51:17 2010 +0100
    33.2 +++ b/src/HOL/Imperative_HOL/ROOT.ML	Wed Dec 29 17:34:41 2010 +0100
    33.3 @@ -1,4 +1,7 @@
    33.4 -
    33.5 -no_document use_thys ["Countable", "Monad_Syntax", "Code_Natural", "LaTeXsugar"];
    33.6 +no_document use_thys [
    33.7 +  "~~/src/HOL/Library/Countable",
    33.8 +  "~~/src/HOL/Library/Monad_Syntax",
    33.9 +  "~~/src/HOL/Library/Code_Natural",
   33.10 +  "~~/src/HOL/Library/LaTeXsugar"];
   33.11  
   33.12  use_thys ["Imperative_HOL_ex"];
    34.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Wed Dec 29 13:51:17 2010 +0100
    34.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Wed Dec 29 17:34:41 2010 +0100
    34.3 @@ -5,7 +5,11 @@
    34.4  header {* An imperative implementation of Quicksort on arrays *}
    34.5  
    34.6  theory Imperative_Quicksort
    34.7 -imports Imperative_HOL Subarray Multiset Efficient_Nat
    34.8 +imports
    34.9 +  Imperative_HOL
   34.10 +  Subarray
   34.11 +  "~~/src/HOL/Library/Multiset"
   34.12 +  "~~/src/HOL/Library/Efficient_Nat"
   34.13  begin
   34.14  
   34.15  text {* We prove QuickSort correct in the Relational Calculus. *}
    35.1 --- a/src/HOL/Imperative_HOL/ex/SatChecker.thy	Wed Dec 29 13:51:17 2010 +0100
    35.2 +++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy	Wed Dec 29 17:34:41 2010 +0100
    35.3 @@ -5,7 +5,7 @@
    35.4  header {* An efficient checker for proofs from a SAT solver *}
    35.5  
    35.6  theory SatChecker
    35.7 -imports RBT_Impl Sorted_List Imperative_HOL
    35.8 +imports "~~/src/HOL/Library/RBT_Impl" Sorted_List Imperative_HOL
    35.9  begin
   35.10  
   35.11  section{* General settings and functions for our representation of clauses *}
    36.1 --- a/src/HOL/Imperative_HOL/ex/Sublist.thy	Wed Dec 29 13:51:17 2010 +0100
    36.2 +++ b/src/HOL/Imperative_HOL/ex/Sublist.thy	Wed Dec 29 17:34:41 2010 +0100
    36.3 @@ -5,7 +5,7 @@
    36.4  header {* Slices of lists *}
    36.5  
    36.6  theory Sublist
    36.7 -imports Multiset
    36.8 +imports "~~/src/HOL/Library/Multiset"
    36.9  begin
   36.10  
   36.11  lemma sublist_split: "i \<le> j \<and> j \<le> k \<Longrightarrow> sublist xs {i..<j} @ sublist xs {j..<k} = sublist xs {i..<k}" 
    37.1 --- a/src/HOL/Import/HOL4Compat.thy	Wed Dec 29 13:51:17 2010 +0100
    37.2 +++ b/src/HOL/Import/HOL4Compat.thy	Wed Dec 29 17:34:41 2010 +0100
    37.3 @@ -3,7 +3,11 @@
    37.4  *)
    37.5  
    37.6  theory HOL4Compat
    37.7 -imports HOL4Setup Complex_Main "~~/src/HOL/Old_Number_Theory/Primes" ContNotDenum
    37.8 +imports
    37.9 +  HOL4Setup
   37.10 +  Complex_Main
   37.11 +  "~~/src/HOL/Old_Number_Theory/Primes"
   37.12 +  "~~/src/HOL/Library/ContNotDenum"
   37.13  begin
   37.14  
   37.15  abbreviation (input) mem (infixl "mem" 55) where "x mem xs \<equiv> List.member xs x"
    38.1 --- a/src/HOL/IsaMakefile	Wed Dec 29 13:51:17 2010 +0100
    38.2 +++ b/src/HOL/IsaMakefile	Wed Dec 29 17:34:41 2010 +0100
    38.3 @@ -1524,7 +1524,7 @@
    38.4  
    38.5  HOLCF-FOCUS: HOLCF $(LOG)/HOLCF-FOCUS.gz
    38.6  
    38.7 -$(LOG)/HOLCF-FOCUS.gz: $(OUT)/HOLCF \
    38.8 +$(LOG)/HOLCF-FOCUS.gz: $(OUT)/HOLCF HOLCF/FOCUS/ROOT.ML \
    38.9    HOLCF/Library/Stream.thy \
   38.10    HOLCF/FOCUS/Fstreams.thy \
   38.11    HOLCF/FOCUS/Fstream.thy \
    39.1 --- a/src/HOL/Isar_Examples/Knaster_Tarski.thy	Wed Dec 29 13:51:17 2010 +0100
    39.2 +++ b/src/HOL/Isar_Examples/Knaster_Tarski.thy	Wed Dec 29 17:34:41 2010 +0100
    39.3 @@ -7,7 +7,7 @@
    39.4  header {* Textbook-style reasoning: the Knaster-Tarski Theorem *}
    39.5  
    39.6  theory Knaster_Tarski
    39.7 -imports Main Lattice_Syntax
    39.8 +imports Main "~~/src/HOL/Library/Lattice_Syntax"
    39.9  begin
   39.10  
   39.11  
    40.1 --- a/src/HOL/Matrix/ComputeFloat.thy	Wed Dec 29 13:51:17 2010 +0100
    40.2 +++ b/src/HOL/Matrix/ComputeFloat.thy	Wed Dec 29 17:34:41 2010 +0100
    40.3 @@ -5,7 +5,7 @@
    40.4  header {* Floating Point Representation of the Reals *}
    40.5  
    40.6  theory ComputeFloat
    40.7 -imports Complex_Main Lattice_Algebras
    40.8 +imports Complex_Main "~~/src/HOL/Library/Lattice_Algebras"
    40.9  uses "~~/src/Tools/float.ML" ("~~/src/HOL/Tools/float_arith.ML")
   40.10  begin
   40.11  
    41.1 --- a/src/HOL/Matrix/LP.thy	Wed Dec 29 13:51:17 2010 +0100
    41.2 +++ b/src/HOL/Matrix/LP.thy	Wed Dec 29 17:34:41 2010 +0100
    41.3 @@ -3,7 +3,7 @@
    41.4  *)
    41.5  
    41.6  theory LP 
    41.7 -imports Main Lattice_Algebras
    41.8 +imports Main "~~/src/HOL/Library/Lattice_Algebras"
    41.9  begin
   41.10  
   41.11  lemma le_add_right_mono: 
    42.1 --- a/src/HOL/Matrix/Matrix.thy	Wed Dec 29 13:51:17 2010 +0100
    42.2 +++ b/src/HOL/Matrix/Matrix.thy	Wed Dec 29 17:34:41 2010 +0100
    42.3 @@ -3,7 +3,7 @@
    42.4  *)
    42.5  
    42.6  theory Matrix
    42.7 -imports Main Lattice_Algebras
    42.8 +imports Main "~~/src/HOL/Library/Lattice_Algebras"
    42.9  begin
   42.10  
   42.11  types 'a infmatrix = "nat \<Rightarrow> nat \<Rightarrow> 'a"
    43.1 --- a/src/HOL/Metis_Examples/Abstraction.thy	Wed Dec 29 13:51:17 2010 +0100
    43.2 +++ b/src/HOL/Metis_Examples/Abstraction.thy	Wed Dec 29 17:34:41 2010 +0100
    43.3 @@ -6,7 +6,7 @@
    43.4  *)
    43.5  
    43.6  theory Abstraction
    43.7 -imports Main FuncSet
    43.8 +imports Main "~~/src/HOL/Library/FuncSet"
    43.9  begin
   43.10  
   43.11  (*For Christoph Benzmueller*)
    44.1 --- a/src/HOL/Metis_Examples/BigO.thy	Wed Dec 29 13:51:17 2010 +0100
    44.2 +++ b/src/HOL/Metis_Examples/BigO.thy	Wed Dec 29 17:34:41 2010 +0100
    44.3 @@ -8,7 +8,11 @@
    44.4  header {* Big O notation *}
    44.5  
    44.6  theory BigO
    44.7 -imports "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Main Function_Algebras Set_Algebras
    44.8 +imports
    44.9 +  "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
   44.10 +  Main
   44.11 +  "~~/src/HOL/Library/Function_Algebras"
   44.12 +  "~~/src/HOL/Library/Set_Algebras"
   44.13  begin
   44.14  
   44.15  subsection {* Definitions *}
    45.1 --- a/src/HOL/Metis_Examples/Tarski.thy	Wed Dec 29 13:51:17 2010 +0100
    45.2 +++ b/src/HOL/Metis_Examples/Tarski.thy	Wed Dec 29 17:34:41 2010 +0100
    45.3 @@ -8,7 +8,7 @@
    45.4  header {* The Full Theorem of Tarski *}
    45.5  
    45.6  theory Tarski
    45.7 -imports Main FuncSet
    45.8 +imports Main "~~/src/HOL/Library/FuncSet"
    45.9  begin
   45.10  
   45.11  (*Many of these higher-order problems appear to be impossible using the
    46.1 --- a/src/HOL/MicroJava/BV/BVExample.thy	Wed Dec 29 13:51:17 2010 +0100
    46.2 +++ b/src/HOL/MicroJava/BV/BVExample.thy	Wed Dec 29 17:34:41 2010 +0100
    46.3 @@ -5,7 +5,11 @@
    46.4  header {* \isaheader{Example Welltypings}\label{sec:BVExample} *}
    46.5  
    46.6  theory BVExample
    46.7 -imports "../JVM/JVMListExample" BVSpecTypeSafe JVM Executable_Set
    46.8 +imports
    46.9 +  "../JVM/JVMListExample"
   46.10 +  BVSpecTypeSafe
   46.11 +  JVM
   46.12 +  "~~/src/HOL/Library/Executable_Set"
   46.13  begin
   46.14  
   46.15  text {*
    47.1 --- a/src/HOL/MicroJava/DFA/Kildall.thy	Wed Dec 29 13:51:17 2010 +0100
    47.2 +++ b/src/HOL/MicroJava/DFA/Kildall.thy	Wed Dec 29 17:34:41 2010 +0100
    47.3 @@ -6,7 +6,7 @@
    47.4  header {* \isaheader{Kildall's Algorithm}\label{sec:Kildall} *}
    47.5  
    47.6  theory Kildall
    47.7 -imports SemilatAlg While_Combinator
    47.8 +imports SemilatAlg "~~/src/HOL/Library/While_Combinator"
    47.9  begin
   47.10  
   47.11  primrec propa :: "'s binop \<Rightarrow> (nat \<times> 's) list \<Rightarrow> 's list \<Rightarrow> nat set \<Rightarrow> 's list * nat set" where
    48.1 --- a/src/HOL/MicroJava/DFA/Semilat.thy	Wed Dec 29 13:51:17 2010 +0100
    48.2 +++ b/src/HOL/MicroJava/DFA/Semilat.thy	Wed Dec 29 17:34:41 2010 +0100
    48.3 @@ -9,7 +9,7 @@
    48.4  *}
    48.5  
    48.6  theory Semilat
    48.7 -imports Main While_Combinator
    48.8 +imports Main "~~/src/HOL/Library/While_Combinator"
    48.9  begin
   48.10  
   48.11  types 
    49.1 --- a/src/HOL/MicroJava/ROOT.ML	Wed Dec 29 13:51:17 2010 +0100
    49.2 +++ b/src/HOL/MicroJava/ROOT.ML	Wed Dec 29 17:34:41 2010 +0100
    49.3 @@ -1,3 +1,3 @@
    49.4 -no_document use_thys ["While_Combinator"];
    49.5 +no_document use_thys ["~~/src/HOL/Library/While_Combinator"];
    49.6  
    49.7  use_thys ["MicroJava"];
    50.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Dec 29 13:51:17 2010 +0100
    50.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Dec 29 17:34:41 2010 +0100
    50.3 @@ -6,7 +6,7 @@
    50.4  header {* Convex sets, functions and related things. *}
    50.5  
    50.6  theory Convex_Euclidean_Space
    50.7 -imports Topology_Euclidean_Space Convex Set_Algebras
    50.8 +imports Topology_Euclidean_Space Convex "~~/src/HOL/Library/Set_Algebras"
    50.9  begin
   50.10  
   50.11  
    51.1 --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Wed Dec 29 13:51:17 2010 +0100
    51.2 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Wed Dec 29 17:34:41 2010 +0100
    51.3 @@ -6,8 +6,12 @@
    51.4  
    51.5  theory Euclidean_Space
    51.6  imports
    51.7 -  Complex_Main "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
    51.8 -  Infinite_Set Inner_Product L2_Norm Convex
    51.9 +  Complex_Main
   51.10 +  "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
   51.11 +  "~~/src/HOL/Library/Infinite_Set"
   51.12 +  "~~/src/HOL/Library/Inner_Product"
   51.13 +  L2_Norm
   51.14 +  "~~/src/HOL/Library/Convex"
   51.15  uses
   51.16    "~~/src/HOL/Library/positivstellensatz.ML"  (* FIXME duplicate use!? *)
   51.17    ("normarith.ML")
    52.1 --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Wed Dec 29 13:51:17 2010 +0100
    52.2 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Wed Dec 29 17:34:41 2010 +0100
    52.3 @@ -5,7 +5,10 @@
    52.4  header {* Definition of finite Cartesian product types. *}
    52.5  
    52.6  theory Finite_Cartesian_Product
    52.7 -imports Inner_Product L2_Norm Numeral_Type
    52.8 +imports
    52.9 +  "~~/src/HOL/Library/Inner_Product"
   52.10 +  L2_Norm
   52.11 +  "~~/src/HOL/Library/Numeral_Type"
   52.12  begin
   52.13  
   52.14  subsection {* Finite Cartesian products, with indexing and lambdas. *}
    53.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Wed Dec 29 13:51:17 2010 +0100
    53.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Wed Dec 29 17:34:41 2010 +0100
    53.3 @@ -4,7 +4,10 @@
    53.4      Translation from HOL light: Robert Himmelmann, TU Muenchen *)
    53.5  
    53.6  theory Integration
    53.7 -  imports Derivative "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Indicator_Function
    53.8 +imports
    53.9 +  Derivative
   53.10 +  "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
   53.11 +  "~~/src/HOL/Library/Indicator_Function"
   53.12  begin
   53.13  
   53.14  declare [[smt_certificates="Integration.certs"]]
    54.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Dec 29 13:51:17 2010 +0100
    54.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Dec 29 17:34:41 2010 +0100
    54.3 @@ -6,7 +6,7 @@
    54.4  header {* Elementary topology in Euclidean space. *}
    54.5  
    54.6  theory Topology_Euclidean_Space
    54.7 -imports SEQ Euclidean_Space Glbs
    54.8 +imports SEQ Euclidean_Space "~~/src/HOL/Library/Glbs"
    54.9  begin
   54.10  
   54.11  (* to be moved elsewhere *)
    55.1 --- a/src/HOL/NSA/NSComplex.thy	Wed Dec 29 13:51:17 2010 +0100
    55.2 +++ b/src/HOL/NSA/NSComplex.thy	Wed Dec 29 17:34:41 2010 +0100
    55.3 @@ -7,7 +7,7 @@
    55.4  header{*Nonstandard Complex Numbers*}
    55.5  
    55.6  theory NSComplex
    55.7 -imports Complex "../Hyperreal/NSA"
    55.8 +imports Complex NSA
    55.9  begin
   55.10  
   55.11  types hcomplex = "complex star"
    56.1 --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Wed Dec 29 13:51:17 2010 +0100
    56.2 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Wed Dec 29 17:34:41 2010 +0100
    56.3 @@ -12,7 +12,7 @@
    56.4     suite. *)
    56.5  
    56.6  theory Manual_Nits
    56.7 -imports Main Quotient_Product RealDef
    56.8 +imports Main "~~/src/HOL/Library/Quotient_Product" RealDef
    56.9  begin
   56.10  
   56.11  chapter {* 3. First Steps *}
    57.1 --- a/src/HOL/Nominal/Nominal.thy	Wed Dec 29 13:51:17 2010 +0100
    57.2 +++ b/src/HOL/Nominal/Nominal.thy	Wed Dec 29 17:34:41 2010 +0100
    57.3 @@ -1,5 +1,5 @@
    57.4  theory Nominal 
    57.5 -imports Main Infinite_Set
    57.6 +imports Main "~~/src/HOL/Library/Infinite_Set"
    57.7  uses
    57.8    ("nominal_thmdecls.ML")
    57.9    ("nominal_atoms.ML")
    58.1 --- a/src/HOL/Nominal/ROOT.ML	Wed Dec 29 13:51:17 2010 +0100
    58.2 +++ b/src/HOL/Nominal/ROOT.ML	Wed Dec 29 17:34:41 2010 +0100
    58.3 @@ -4,5 +4,5 @@
    58.4  The nominal datatype package.
    58.5  *)
    58.6  
    58.7 -no_document use_thys ["Infinite_Set"];
    58.8 +no_document use_thys ["~~/src/HOL/Library/Infinite_Set"];
    58.9  use_thys ["Nominal"];
    59.1 --- a/src/HOL/Number_Theory/UniqueFactorization.thy	Wed Dec 29 13:51:17 2010 +0100
    59.2 +++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Wed Dec 29 17:34:41 2010 +0100
    59.3 @@ -12,7 +12,7 @@
    59.4  header {* UniqueFactorization *}
    59.5  
    59.6  theory UniqueFactorization
    59.7 -imports Cong Multiset
    59.8 +imports Cong "~~/src/HOL/Library/Multiset"
    59.9  begin
   59.10  
   59.11  (* inherited from Multiset *)
    60.1 --- a/src/HOL/Old_Number_Theory/Factorization.thy	Wed Dec 29 13:51:17 2010 +0100
    60.2 +++ b/src/HOL/Old_Number_Theory/Factorization.thy	Wed Dec 29 17:34:41 2010 +0100
    60.3 @@ -6,7 +6,7 @@
    60.4  header {* Fundamental Theorem of Arithmetic (unique factorization into primes) *}
    60.5  
    60.6  theory Factorization
    60.7 -imports Primes Permutation
    60.8 +imports Primes "~~/src/HOL/Library/Permutation"
    60.9  begin
   60.10  
   60.11  
    61.1 --- a/src/HOL/Old_Number_Theory/Finite2.thy	Wed Dec 29 13:51:17 2010 +0100
    61.2 +++ b/src/HOL/Old_Number_Theory/Finite2.thy	Wed Dec 29 17:34:41 2010 +0100
    61.3 @@ -5,7 +5,7 @@
    61.4  header {*Finite Sets and Finite Sums*}
    61.5  
    61.6  theory Finite2
    61.7 -imports IntFact Infinite_Set
    61.8 +imports IntFact "~~/src/HOL/Library/Infinite_Set"
    61.9  begin
   61.10  
   61.11  text{*
    62.1 --- a/src/HOL/Old_Number_Theory/ROOT.ML	Wed Dec 29 13:51:17 2010 +0100
    62.2 +++ b/src/HOL/Old_Number_Theory/ROOT.ML	Wed Dec 29 17:34:41 2010 +0100
    62.3 @@ -1,4 +1,15 @@
    62.4 +no_document use_thys [
    62.5 +  "~~/src/HOL/Library/Infinite_Set",
    62.6 +  "~~/src/HOL/Library/Permutation"
    62.7 +];
    62.8  
    62.9 -no_document use_thys ["Infinite_Set", "Permutation"];
   62.10 -use_thys ["Fib", "Factorization", "Chinese", "WilsonRuss",
   62.11 -  "WilsonBij", "Quadratic_Reciprocity", "Primes", "Pocklington"];
   62.12 +use_thys [
   62.13 +  "Fib",
   62.14 +  "Factorization",
   62.15 +  "Chinese",
   62.16 +  "WilsonRuss",
   62.17 +  "WilsonBij",
   62.18 +  "Quadratic_Reciprocity",
   62.19 +  "Primes",
   62.20 +  "Pocklington"
   62.21 +];
    63.1 --- a/src/HOL/Predicate_Compile_Examples/Examples.thy	Wed Dec 29 13:51:17 2010 +0100
    63.2 +++ b/src/HOL/Predicate_Compile_Examples/Examples.thy	Wed Dec 29 17:34:41 2010 +0100
    63.3 @@ -1,5 +1,5 @@
    63.4  theory Examples
    63.5 -imports Main Predicate_Compile_Alternative_Defs
    63.6 +imports Main "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs"
    63.7  begin
    63.8  
    63.9  section {* Formal Languages *}
    64.1 --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	Wed Dec 29 13:51:17 2010 +0100
    64.2 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	Wed Dec 29 17:34:41 2010 +0100
    64.3 @@ -1,5 +1,5 @@
    64.4  theory Hotel_Example_Prolog
    64.5 -imports Hotel_Example Predicate_Compile_Alternative_Defs Code_Prolog
    64.6 +imports Hotel_Example "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs" Code_Prolog
    64.7  begin
    64.8  
    64.9  declare Let_def[code_pred_inline]
    65.1 --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy	Wed Dec 29 13:51:17 2010 +0100
    65.2 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy	Wed Dec 29 17:34:41 2010 +0100
    65.3 @@ -1,5 +1,5 @@
    65.4  theory Hotel_Example_Small_Generator
    65.5 -imports Hotel_Example Predicate_Compile_Alternative_Defs
    65.6 +imports Hotel_Example "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs"
    65.7  uses "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML"
    65.8  begin
    65.9  
    66.1 --- a/src/HOL/Predicate_Compile_Examples/IMP_1.thy	Wed Dec 29 13:51:17 2010 +0100
    66.2 +++ b/src/HOL/Predicate_Compile_Examples/IMP_1.thy	Wed Dec 29 17:34:41 2010 +0100
    66.3 @@ -1,5 +1,5 @@
    66.4  theory IMP_1
    66.5 -imports "Predicate_Compile_Quickcheck"
    66.6 +imports "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
    66.7  begin
    66.8  
    66.9  subsection {* IMP *}
    67.1 --- a/src/HOL/Predicate_Compile_Examples/IMP_2.thy	Wed Dec 29 13:51:17 2010 +0100
    67.2 +++ b/src/HOL/Predicate_Compile_Examples/IMP_2.thy	Wed Dec 29 17:34:41 2010 +0100
    67.3 @@ -1,5 +1,5 @@
    67.4  theory IMP_2
    67.5 -imports "Predicate_Compile_Quickcheck"
    67.6 +imports "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
    67.7  begin
    67.8  
    67.9  subsection {* IMP *}
    68.1 --- a/src/HOL/Predicate_Compile_Examples/IMP_3.thy	Wed Dec 29 13:51:17 2010 +0100
    68.2 +++ b/src/HOL/Predicate_Compile_Examples/IMP_3.thy	Wed Dec 29 17:34:41 2010 +0100
    68.3 @@ -1,5 +1,5 @@
    68.4  theory IMP_3
    68.5 -imports "Predicate_Compile_Quickcheck"
    68.6 +imports "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
    68.7  begin
    68.8  
    68.9  subsection {* IMP *}
    69.1 --- a/src/HOL/Predicate_Compile_Examples/IMP_4.thy	Wed Dec 29 13:51:17 2010 +0100
    69.2 +++ b/src/HOL/Predicate_Compile_Examples/IMP_4.thy	Wed Dec 29 17:34:41 2010 +0100
    69.3 @@ -1,5 +1,5 @@
    69.4  theory IMP_4
    69.5 -imports Predicate_Compile_Quickcheck
    69.6 +imports "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
    69.7  begin
    69.8  
    69.9  subsection {* IMP *}
    70.1 --- a/src/HOL/Predicate_Compile_Examples/List_Examples.thy	Wed Dec 29 13:51:17 2010 +0100
    70.2 +++ b/src/HOL/Predicate_Compile_Examples/List_Examples.thy	Wed Dec 29 17:34:41 2010 +0100
    70.3 @@ -1,5 +1,5 @@
    70.4  theory List_Examples
    70.5 -imports Main "Predicate_Compile_Quickcheck" "Code_Prolog"
    70.6 +imports Main "~~/src/HOL/Library/Predicate_Compile_Quickcheck" "Code_Prolog"
    70.7  begin
    70.8  
    70.9  setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *}
    71.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Wed Dec 29 13:51:17 2010 +0100
    71.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Wed Dec 29 17:34:41 2010 +0100
    71.3 @@ -1,5 +1,5 @@
    71.4  theory Predicate_Compile_Quickcheck_Examples
    71.5 -imports Predicate_Compile_Quickcheck
    71.6 +imports "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
    71.7  begin
    71.8  
    71.9  section {* Sets *}
    72.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Wed Dec 29 13:51:17 2010 +0100
    72.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Wed Dec 29 17:34:41 2010 +0100
    72.3 @@ -1,5 +1,5 @@
    72.4  theory Predicate_Compile_Tests
    72.5 -imports Predicate_Compile_Alternative_Defs
    72.6 +imports "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs"
    72.7  begin
    72.8  
    72.9  subsection {* Basic predicates *}
    73.1 --- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Wed Dec 29 13:51:17 2010 +0100
    73.2 +++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Wed Dec 29 17:34:41 2010 +0100
    73.3 @@ -1,5 +1,5 @@
    73.4  theory Reg_Exp_Example
    73.5 -imports Predicate_Compile_Quickcheck Code_Prolog
    73.6 +imports "~~/src/HOL/Library/Predicate_Compile_Quickcheck" Code_Prolog
    73.7  begin
    73.8  
    73.9  text {* An example from the experiments from SmallCheck (http://www.cs.york.ac.uk/fp/smallcheck/) *}
    74.1 --- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Wed Dec 29 13:51:17 2010 +0100
    74.2 +++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Wed Dec 29 17:34:41 2010 +0100
    74.3 @@ -1,5 +1,5 @@
    74.4  theory Specialisation_Examples
    74.5 -imports Main Predicate_Compile_Alternative_Defs
    74.6 +imports Main "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs"
    74.7  begin
    74.8  
    74.9  section {* Specialisation Examples *}
    75.1 --- a/src/HOL/Probability/Information.thy	Wed Dec 29 13:51:17 2010 +0100
    75.2 +++ b/src/HOL/Probability/Information.thy	Wed Dec 29 17:34:41 2010 +0100
    75.3 @@ -1,5 +1,8 @@
    75.4  theory Information
    75.5 -imports Probability_Space Convex Lebesgue_Measure
    75.6 +imports
    75.7 +  Probability_Space
    75.8 +  "~~/src/HOL/Library/Convex"
    75.9 +  Lebesgue_Measure
   75.10  begin
   75.11  
   75.12  lemma log_le: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> x \<le> y \<Longrightarrow> log a x \<le> log a y"
    76.1 --- a/src/HOL/Probability/Positive_Extended_Real.thy	Wed Dec 29 13:51:17 2010 +0100
    76.2 +++ b/src/HOL/Probability/Positive_Extended_Real.thy	Wed Dec 29 17:34:41 2010 +0100
    76.3 @@ -3,7 +3,7 @@
    76.4  header {* A type for positive real numbers with infinity *}
    76.5  
    76.6  theory Positive_Extended_Real
    76.7 -  imports Complex_Main Nat_Bijection Multivariate_Analysis
    76.8 +  imports Complex_Main "~~/src/HOL/Library/Nat_Bijection" Multivariate_Analysis
    76.9  begin
   76.10  
   76.11  lemma (in complete_lattice) Sup_start:
    77.1 --- a/src/HOL/Probability/Sigma_Algebra.thy	Wed Dec 29 13:51:17 2010 +0100
    77.2 +++ b/src/HOL/Probability/Sigma_Algebra.thy	Wed Dec 29 17:34:41 2010 +0100
    77.3 @@ -6,7 +6,13 @@
    77.4  
    77.5  header {* Sigma Algebras *}
    77.6  
    77.7 -theory Sigma_Algebra imports Main Countable FuncSet Indicator_Function begin
    77.8 +theory Sigma_Algebra
    77.9 +imports
   77.10 +  Main
   77.11 +  "~~/src/HOL/Library/Countable"
   77.12 +  "~~/src/HOL/Library/FuncSet"
   77.13 +  "~~/src/HOL/Library/Indicator_Function"
   77.14 +begin
   77.15  
   77.16  text {* Sigma algebras are an elementary concept in measure
   77.17    theory. To measure --- that is to integrate --- functions, we first have
    78.1 --- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Wed Dec 29 13:51:17 2010 +0100
    78.2 +++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Wed Dec 29 17:34:41 2010 +0100
    78.3 @@ -3,7 +3,7 @@
    78.4  header {* Formalization of a Countermeasure by Koepf & Duermuth 2009 *}
    78.5  
    78.6  theory Koepf_Duermuth_Countermeasure
    78.7 -  imports Information Permutation
    78.8 +  imports Information "~~/src/HOL/Library/Permutation"
    78.9  begin
   78.10  
   78.11  lemma
    79.1 --- a/src/HOL/Proofs/Extraction/Euclid.thy	Wed Dec 29 13:51:17 2010 +0100
    79.2 +++ b/src/HOL/Proofs/Extraction/Euclid.thy	Wed Dec 29 17:34:41 2010 +0100
    79.3 @@ -7,7 +7,10 @@
    79.4  header {* Euclid's theorem *}
    79.5  
    79.6  theory Euclid
    79.7 -imports "~~/src/HOL/Number_Theory/UniqueFactorization" Util Efficient_Nat
    79.8 +imports
    79.9 +  "~~/src/HOL/Number_Theory/UniqueFactorization"
   79.10 +  Util
   79.11 +  "~~/src/HOL/Library/Efficient_Nat"
   79.12  begin
   79.13  
   79.14  text {*
    80.1 --- a/src/HOL/Proofs/Extraction/Higman.thy	Wed Dec 29 13:51:17 2010 +0100
    80.2 +++ b/src/HOL/Proofs/Extraction/Higman.thy	Wed Dec 29 17:34:41 2010 +0100
    80.3 @@ -6,7 +6,7 @@
    80.4  header {* Higman's lemma *}
    80.5  
    80.6  theory Higman
    80.7 -imports Main State_Monad Random
    80.8 +imports Main "~~/src/HOL/Library/State_Monad" Random
    80.9  begin
   80.10  
   80.11  text {*
    81.1 --- a/src/HOL/Proofs/Extraction/Pigeonhole.thy	Wed Dec 29 13:51:17 2010 +0100
    81.2 +++ b/src/HOL/Proofs/Extraction/Pigeonhole.thy	Wed Dec 29 17:34:41 2010 +0100
    81.3 @@ -5,7 +5,7 @@
    81.4  header {* The pigeonhole principle *}
    81.5  
    81.6  theory Pigeonhole
    81.7 -imports Util Efficient_Nat
    81.8 +imports Util "~~/src/HOL/Library/Efficient_Nat"
    81.9  begin
   81.10  
   81.11  text {*
    82.1 --- a/src/HOL/Proofs/Extraction/ROOT.ML	Wed Dec 29 13:51:17 2010 +0100
    82.2 +++ b/src/HOL/Proofs/Extraction/ROOT.ML	Wed Dec 29 17:34:41 2010 +0100
    82.3 @@ -1,6 +1,12 @@
    82.4  (* Examples for program extraction in Higher-Order Logic *)
    82.5  
    82.6 -no_document use_thys ["Efficient_Nat", "Monad_Syntax", "~~/src/HOL/Number_Theory/Primes"];
    82.7 +no_document use_thys [
    82.8 +  "~~/src/HOL/Library/Efficient_Nat",
    82.9 +  "~~/src/HOL/Library/Monad_Syntax",
   82.10 +  "~~/src/HOL/Number_Theory/Primes"
   82.11 +];
   82.12 +
   82.13  share_common_data ();
   82.14 +
   82.15  no_document use_thys ["~~/src/HOL/Number_Theory/UniqueFactorization"];
   82.16  use_thys ["Greatest_Common_Divisor", "Warshall", "Higman", "Pigeonhole", "Euclid"];
    83.1 --- a/src/HOL/Proofs/Lambda/ROOT.ML	Wed Dec 29 13:51:17 2010 +0100
    83.2 +++ b/src/HOL/Proofs/Lambda/ROOT.ML	Wed Dec 29 17:34:41 2010 +0100
    83.3 @@ -1,2 +1,2 @@
    83.4 -no_document use_thys ["Code_Integer"];
    83.5 +no_document use_thys ["~~/src/HOL/Library/Code_Integer"];
    83.6  use_thys ["Eta", "StrongNorm", "Standardization", "WeakNorm"];
    84.1 --- a/src/HOL/Proofs/Lambda/WeakNorm.thy	Wed Dec 29 13:51:17 2010 +0100
    84.2 +++ b/src/HOL/Proofs/Lambda/WeakNorm.thy	Wed Dec 29 17:34:41 2010 +0100
    84.3 @@ -6,7 +6,7 @@
    84.4  header {* Weak normalization for simply-typed lambda calculus *}
    84.5  
    84.6  theory WeakNorm
    84.7 -imports Type NormalForm Code_Integer
    84.8 +imports Type NormalForm "~~/src/HOL/Library/Code_Integer"
    84.9  begin
   84.10  
   84.11  text {*
    85.1 --- a/src/HOL/Quotient_Examples/FSet.thy	Wed Dec 29 13:51:17 2010 +0100
    85.2 +++ b/src/HOL/Quotient_Examples/FSet.thy	Wed Dec 29 17:34:41 2010 +0100
    85.3 @@ -6,7 +6,7 @@
    85.4  *)
    85.5  
    85.6  theory FSet
    85.7 -imports Quotient_List More_List
    85.8 +imports "~~/src/HOL/Library/Quotient_List" "~~/src/HOL/Library/More_List"
    85.9  begin
   85.10  
   85.11  text {* 
    86.1 --- a/src/HOL/Quotient_Examples/Quotient_Int.thy	Wed Dec 29 13:51:17 2010 +0100
    86.2 +++ b/src/HOL/Quotient_Examples/Quotient_Int.thy	Wed Dec 29 17:34:41 2010 +0100
    86.3 @@ -5,7 +5,7 @@
    86.4  Integers based on Quotients, based on an older version by Larry Paulson.
    86.5  *)
    86.6  theory Quotient_Int
    86.7 -imports Quotient_Product Nat
    86.8 +imports "~~/src/HOL/Library/Quotient_Product" Nat
    86.9  begin
   86.10  
   86.11  fun
    87.1 --- a/src/HOL/SET_Protocol/Message_SET.thy	Wed Dec 29 13:51:17 2010 +0100
    87.2 +++ b/src/HOL/SET_Protocol/Message_SET.thy	Wed Dec 29 17:34:41 2010 +0100
    87.3 @@ -7,7 +7,7 @@
    87.4  header{*The Message Theory, Modified for SET*}
    87.5  
    87.6  theory Message_SET
    87.7 -imports Main Nat_Bijection
    87.8 +imports Main "~~/src/HOL/Library/Nat_Bijection"
    87.9  begin
   87.10  
   87.11  subsection{*General Lemmas*}
    88.1 --- a/src/HOL/SET_Protocol/ROOT.ML	Wed Dec 29 13:51:17 2010 +0100
    88.2 +++ b/src/HOL/SET_Protocol/ROOT.ML	Wed Dec 29 17:34:41 2010 +0100
    88.3 @@ -1,3 +1,2 @@
    88.4 -
    88.5 -no_document use_thys ["Nat_Bijection"];
    88.6 +no_document use_thys ["~~/src/HOL/Library/Nat_Bijection"];
    88.7  use_thys ["SET_Protocol"];
    89.1 --- a/src/HOL/UNITY/Follows.thy	Wed Dec 29 13:51:17 2010 +0100
    89.2 +++ b/src/HOL/UNITY/Follows.thy	Wed Dec 29 17:34:41 2010 +0100
    89.3 @@ -5,7 +5,9 @@
    89.4  
    89.5  header{*The Follows Relation of Charpentier and Sivilotte*}
    89.6  
    89.7 -theory Follows imports SubstAx ListOrder Multiset begin
    89.8 +theory Follows
    89.9 +imports SubstAx ListOrder "~~/src/HOL/Library/Multiset"
   89.10 +begin
   89.11  
   89.12  definition Follows :: "['a => 'b::{order}, 'a => 'b::{order}] => 'a program set" (infixl "Fols" 65) where
   89.13     "f Fols g == Increasing g \<inter> Increasing f Int
    90.1 --- a/src/HOL/Unix/Unix.thy	Wed Dec 29 13:51:17 2010 +0100
    90.2 +++ b/src/HOL/Unix/Unix.thy	Wed Dec 29 17:34:41 2010 +0100
    90.3 @@ -5,7 +5,10 @@
    90.4  header {* Unix file-systems \label{sec:unix-file-system} *}
    90.5  
    90.6  theory Unix
    90.7 -imports Main Nested_Environment List_Prefix
    90.8 +imports
    90.9 +  Main
   90.10 +  "~~/src/HOL/Library/Nested_Environment"
   90.11 +  "~~/src/HOL/Library/List_Prefix"
   90.12  begin
   90.13  
   90.14  text {*
    91.1 --- a/src/HOL/Word/Bit_Operations.thy	Wed Dec 29 13:51:17 2010 +0100
    91.2 +++ b/src/HOL/Word/Bit_Operations.thy	Wed Dec 29 17:34:41 2010 +0100
    91.3 @@ -5,7 +5,7 @@
    91.4  header {* Syntactic classes for bitwise operations *}
    91.5  
    91.6  theory Bit_Operations
    91.7 -imports Bit
    91.8 +imports "~~/src/HOL/Library/Bit"
    91.9  begin
   91.10  
   91.11  class bit =
    92.1 --- a/src/HOL/Word/Bit_Representation.thy	Wed Dec 29 13:51:17 2010 +0100
    92.2 +++ b/src/HOL/Word/Bit_Representation.thy	Wed Dec 29 17:34:41 2010 +0100
    92.3 @@ -8,7 +8,7 @@
    92.4  header {* Basic Definitions for Binary Integers *}
    92.5  
    92.6  theory Bit_Representation
    92.7 -imports Misc_Numeric Bit
    92.8 +imports Misc_Numeric "~~/src/HOL/Library/Bit"
    92.9  begin
   92.10  
   92.11  subsection {* Further properties of numerals *}
    93.1 --- a/src/HOL/Word/Type_Length.thy	Wed Dec 29 13:51:17 2010 +0100
    93.2 +++ b/src/HOL/Word/Type_Length.thy	Wed Dec 29 17:34:41 2010 +0100
    93.3 @@ -5,7 +5,7 @@
    93.4  header {* Assigning lengths to types by typeclasses *}
    93.5  
    93.6  theory Type_Length
    93.7 -imports Numeral_Type
    93.8 +imports "~~/src/HOL/Library/Numeral_Type"
    93.9  begin
   93.10  
   93.11  text {*
    94.1 --- a/src/HOL/Word/Word.thy	Wed Dec 29 13:51:17 2010 +0100
    94.2 +++ b/src/HOL/Word/Word.thy	Wed Dec 29 17:34:41 2010 +0100
    94.3 @@ -5,7 +5,11 @@
    94.4  header {* A type of finite bit strings *}
    94.5  
    94.6  theory Word
    94.7 -imports Type_Length Misc_Typedef Boolean_Algebra Bool_List_Representation
    94.8 +imports
    94.9 +  Type_Length
   94.10 +  Misc_Typedef
   94.11 +  "~~/src/HOL/Library/Boolean_Algebra"
   94.12 +  Bool_List_Representation
   94.13  uses ("~~/src/HOL/Word/Tools/smt_word.ML")
   94.14  begin
   94.15  
    95.1 --- a/src/HOL/ZF/LProd.thy	Wed Dec 29 13:51:17 2010 +0100
    95.2 +++ b/src/HOL/ZF/LProd.thy	Wed Dec 29 17:34:41 2010 +0100
    95.3 @@ -6,7 +6,7 @@
    95.4  *)
    95.5  
    95.6  theory LProd 
    95.7 -imports Multiset
    95.8 +imports "~~/src/HOL/Library/Multiset"
    95.9  begin
   95.10  
   95.11  inductive_set
    96.1 --- a/src/HOL/ex/Efficient_Nat_examples.thy	Wed Dec 29 13:51:17 2010 +0100
    96.2 +++ b/src/HOL/ex/Efficient_Nat_examples.thy	Wed Dec 29 17:34:41 2010 +0100
    96.3 @@ -5,7 +5,7 @@
    96.4  header {* Simple examples for Efficient\_Nat theory. *}
    96.5  
    96.6  theory Efficient_Nat_examples
    96.7 -imports Complex_Main Efficient_Nat
    96.8 +imports Complex_Main "~~/src/HOL/Library/Efficient_Nat"
    96.9  begin
   96.10  
   96.11  fun to_n :: "nat \<Rightarrow> nat list" where
    97.1 --- a/src/HOL/ex/Execute_Choice.thy	Wed Dec 29 13:51:17 2010 +0100
    97.2 +++ b/src/HOL/ex/Execute_Choice.thy	Wed Dec 29 17:34:41 2010 +0100
    97.3 @@ -3,7 +3,7 @@
    97.4  header {* A simple cookbook example how to eliminate choice in programs. *}
    97.5  
    97.6  theory Execute_Choice
    97.7 -imports Main AssocList
    97.8 +imports Main "~~/src/HOL/Library/AssocList"
    97.9  begin
   97.10  
   97.11  text {*
    98.1 --- a/src/HOL/ex/Fundefs.thy	Wed Dec 29 13:51:17 2010 +0100
    98.2 +++ b/src/HOL/ex/Fundefs.thy	Wed Dec 29 17:34:41 2010 +0100
    98.3 @@ -5,7 +5,7 @@
    98.4  header {* Examples of function definitions *}
    98.5  
    98.6  theory Fundefs 
    98.7 -imports Parity Monad_Syntax
    98.8 +imports Parity "~~/src/HOL/Library/Monad_Syntax"
    98.9  begin
   98.10  
   98.11  subsection {* Very basic *}
    99.1 --- a/src/HOL/ex/Landau.thy	Wed Dec 29 13:51:17 2010 +0100
    99.2 +++ b/src/HOL/ex/Landau.thy	Wed Dec 29 17:34:41 2010 +0100
    99.3 @@ -4,7 +4,7 @@
    99.4  header {* Comparing growth of functions on natural numbers by a preorder relation *}
    99.5  
    99.6  theory Landau
    99.7 -imports Main Preorder
    99.8 +imports Main "~~/src/HOL/Library/Preorder"
    99.9  begin
   99.10  
   99.11  text {*
   100.1 --- a/src/HOL/ex/MergeSort.thy	Wed Dec 29 13:51:17 2010 +0100
   100.2 +++ b/src/HOL/ex/MergeSort.thy	Wed Dec 29 17:34:41 2010 +0100
   100.3 @@ -6,7 +6,7 @@
   100.4  header{*Merge Sort*}
   100.5  
   100.6  theory MergeSort
   100.7 -imports Multiset
   100.8 +imports "~~/src/HOL/Library/Multiset"
   100.9  begin
  100.10  
  100.11  context linorder
   101.1 --- a/src/HOL/ex/Quickcheck_Lattice_Examples.thy	Wed Dec 29 13:51:17 2010 +0100
   101.2 +++ b/src/HOL/ex/Quickcheck_Lattice_Examples.thy	Wed Dec 29 17:34:41 2010 +0100
   101.3 @@ -4,7 +4,7 @@
   101.4  *)
   101.5  
   101.6  theory Quickcheck_Lattice_Examples
   101.7 -imports Quickcheck_Types
   101.8 +imports "~~/src/HOL/Library/Quickcheck_Types"
   101.9  begin
  101.10  
  101.11  text {* We show how other default types help to find counterexamples to propositions if
   102.1 --- a/src/HOL/ex/Quicksort.thy	Wed Dec 29 13:51:17 2010 +0100
   102.2 +++ b/src/HOL/ex/Quicksort.thy	Wed Dec 29 17:34:41 2010 +0100
   102.3 @@ -5,7 +5,7 @@
   102.4  header {* Quicksort with function package *}
   102.5  
   102.6  theory Quicksort
   102.7 -imports Main Multiset
   102.8 +imports Main "~~/src/HOL/Library/Multiset"
   102.9  begin
  102.10  
  102.11  context linorder
   103.1 --- a/src/HOL/ex/ROOT.ML	Wed Dec 29 13:51:17 2010 +0100
   103.2 +++ b/src/HOL/ex/ROOT.ML	Wed Dec 29 17:34:41 2010 +0100
   103.3 @@ -4,9 +4,9 @@
   103.4  *)
   103.5  
   103.6  no_document use_thys [
   103.7 -  "State_Monad",
   103.8 +  "~~/src/HOL/Library/State_Monad",
   103.9    "Efficient_Nat_examples",
  103.10 -  "FuncSet",
  103.11 +  "~~/src/HOL/Library/FuncSet",
  103.12    "Eval_Examples",
  103.13    "Normalization_by_Evaluation",
  103.14    "Hebrew",
   104.1 --- a/src/HOL/ex/ReflectionEx.thy	Wed Dec 29 13:51:17 2010 +0100
   104.2 +++ b/src/HOL/ex/ReflectionEx.thy	Wed Dec 29 17:34:41 2010 +0100
   104.3 @@ -5,7 +5,7 @@
   104.4  header {* Examples for generic reflection and reification *}
   104.5  
   104.6  theory ReflectionEx
   104.7 -imports Reflection
   104.8 +imports "~~/src/HOL/Library/Reflection"
   104.9  begin
  104.10  
  104.11  text{* This theory presents two methods: reify and reflection *}
   105.1 --- a/src/HOL/ex/Sorting.thy	Wed Dec 29 13:51:17 2010 +0100
   105.2 +++ b/src/HOL/ex/Sorting.thy	Wed Dec 29 17:34:41 2010 +0100
   105.3 @@ -7,7 +7,7 @@
   105.4  header{*Sorting: Basic Theory*}
   105.5  
   105.6  theory Sorting
   105.7 -imports Main Multiset
   105.8 +imports Main "~~/src/HOL/Library/Multiset"
   105.9  begin
  105.10  
  105.11  consts
   106.1 --- a/src/HOL/ex/Tarski.thy	Wed Dec 29 13:51:17 2010 +0100
   106.2 +++ b/src/HOL/ex/Tarski.thy	Wed Dec 29 17:34:41 2010 +0100
   106.3 @@ -1,12 +1,11 @@
   106.4  (*  Title:      HOL/ex/Tarski.thy
   106.5 -    ID:         $Id$
   106.6      Author:     Florian Kammüller, Cambridge University Computer Laboratory
   106.7  *)
   106.8  
   106.9  header {* The Full Theorem of Tarski *}
  106.10  
  106.11  theory Tarski
  106.12 -imports Main FuncSet
  106.13 +imports Main "~~/src/HOL/Library/FuncSet"
  106.14  begin
  106.15  
  106.16  text {*
   107.1 --- a/src/HOL/ex/Termination.thy	Wed Dec 29 13:51:17 2010 +0100
   107.2 +++ b/src/HOL/ex/Termination.thy	Wed Dec 29 17:34:41 2010 +0100
   107.3 @@ -6,7 +6,7 @@
   107.4  header {* Examples and regression tests for automated termination proofs *}
   107.5   
   107.6  theory Termination
   107.7 -imports Main Multiset
   107.8 +imports Main "~~/src/HOL/Library/Multiset"
   107.9  begin
  107.10  
  107.11  subsection {* Manually giving termination relations using @{text relation} and
   108.1 --- a/src/HOL/ex/ThreeDivides.thy	Wed Dec 29 13:51:17 2010 +0100
   108.2 +++ b/src/HOL/ex/ThreeDivides.thy	Wed Dec 29 17:34:41 2010 +0100
   108.3 @@ -5,7 +5,7 @@
   108.4  header {* Three Divides Theorem *}
   108.5  
   108.6  theory ThreeDivides
   108.7 -imports Main LaTeXsugar
   108.8 +imports Main "~~/src/HOL/Library/LaTeXsugar"
   108.9  begin
  108.10  
  108.11  subsection {* Abstract *}
   109.1 --- a/src/HOL/ex/While_Combinator_Example.thy	Wed Dec 29 13:51:17 2010 +0100
   109.2 +++ b/src/HOL/ex/While_Combinator_Example.thy	Wed Dec 29 17:34:41 2010 +0100
   109.3 @@ -6,7 +6,7 @@
   109.4  header {* An application of the While combinator *}
   109.5  
   109.6  theory While_Combinator_Example
   109.7 -imports While_Combinator
   109.8 +imports "~~/src/HOL/Library/While_Combinator"
   109.9  begin
  109.10  
  109.11  text {* Computation of the @{term lfp} on finite sets via