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