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