--- a/src/HOL/Library/Combine_PER.thy Mon Apr 03 23:31:31 2017 +0200
+++ b/src/HOL/Library/Combine_PER.thy Tue Apr 04 11:52:28 2017 +0200
@@ -3,7 +3,7 @@
section \<open>A combinator to build partial equivalence relations from a predicate and an equivalence relation\<close>
theory Combine_PER
- imports Main "~~/src/HOL/Library/Lattice_Syntax"
+ imports Main Lattice_Syntax
begin
definition combine_per :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
--- a/src/HOL/Library/Complete_Partial_Order2.thy Mon Apr 03 23:31:31 2017 +0200
+++ b/src/HOL/Library/Complete_Partial_Order2.thy Tue Apr 04 11:52:28 2017 +0200
@@ -5,8 +5,7 @@
section \<open>Formalisation of chain-complete partial orders, continuity and admissibility\<close>
theory Complete_Partial_Order2 imports
- Main
- "~~/src/HOL/Library/Lattice_Syntax"
+ Main Lattice_Syntax
begin
lemma chain_transfer [transfer_rule]:
--- a/src/HOL/Library/Extended.thy Mon Apr 03 23:31:31 2017 +0200
+++ b/src/HOL/Library/Extended.thy Tue Apr 04 11:52:28 2017 +0200
@@ -5,9 +5,7 @@
*)
theory Extended
-imports
- Main
- "~~/src/HOL/Library/Simps_Case_Conv"
+ imports Simps_Case_Conv
begin
datatype 'a extended = Fin 'a | Pinf ("\<infinity>") | Minf ("-\<infinity>")
--- a/src/HOL/Library/Multiset_Permutations.thy Mon Apr 03 23:31:31 2017 +0200
+++ b/src/HOL/Library/Multiset_Permutations.thy Tue Apr 04 11:52:28 2017 +0200
@@ -1,16 +1,17 @@
-(*
- File: Multiset_Permutations.thy
- Author: Manuel Eberl (TU München)
+(* Title: HOL/Library/Multiset_Permutations.thy
+ Author: Manuel Eberl (TU München)
- Defines the set of permutations of a given multiset (or set), i.e. the set of all lists whose
- entries correspond to the multiset (resp. set).
+Defines the set of permutations of a given multiset (or set), i.e. the set of all lists whose
+entries correspond to the multiset (resp. set).
*)
+
section \<open>Permutations of a Multiset\<close>
+
theory Multiset_Permutations
imports
Complex_Main
- "~~/src/HOL/Library/Multiset"
- "~~/src/HOL/Library/Permutations"
+ Multiset
+ Permutations
begin
(* TODO Move *)
--- a/src/HOL/Library/Normalized_Fraction.thy Mon Apr 03 23:31:31 2017 +0200
+++ b/src/HOL/Library/Normalized_Fraction.thy Tue Apr 04 11:52:28 2017 +0200
@@ -6,7 +6,7 @@
imports
Main
"~~/src/HOL/Number_Theory/Euclidean_Algorithm"
- "~~/src/HOL/Library/Fraction_Field"
+ Fraction_Field
begin
definition quot_to_fract :: "'a :: {idom} \<times> 'a \<Rightarrow> 'a fract" where
--- a/src/HOL/Library/Polynomial.thy Mon Apr 03 23:31:31 2017 +0200
+++ b/src/HOL/Library/Polynomial.thy Tue Apr 04 11:52:28 2017 +0200
@@ -10,8 +10,8 @@
theory Polynomial
imports
"~~/src/HOL/Deriv"
- "~~/src/HOL/Library/More_List"
- "~~/src/HOL/Library/Infinite_Set"
+ More_List
+ Infinite_Set
begin
subsection \<open>Auxiliary: operations for lists (later) representing coefficients\<close>
--- a/src/HOL/Library/Polynomial_FPS.thy Mon Apr 03 23:31:31 2017 +0200
+++ b/src/HOL/Library/Polynomial_FPS.thy Tue Apr 04 11:52:28 2017 +0200
@@ -1,13 +1,13 @@
-(*
- File: Polynomial_FPS.thy
- Author: Manuel Eberl (TUM)
+(* Title: HOL/Library/Polynomial_FPS.thy
+ Author: Manuel Eberl, TU München
- Converting polynomials to formal power series
+Converting polynomials to formal power series.
*)
section \<open>Converting polynomials to formal power series\<close>
+
theory Polynomial_FPS
-imports Polynomial Formal_Power_Series
+ imports Polynomial Formal_Power_Series
begin
definition fps_of_poly where
--- a/src/HOL/Library/Polynomial_Factorial.thy Mon Apr 03 23:31:31 2017 +0200
+++ b/src/HOL/Library/Polynomial_Factorial.thy Tue Apr 04 11:52:28 2017 +0200
@@ -9,9 +9,9 @@
theory Polynomial_Factorial
imports
Complex_Main
- "~~/src/HOL/Library/Polynomial"
- "~~/src/HOL/Library/Normalized_Fraction"
- "~~/src/HOL/Library/Field_as_Ring"
+ Polynomial
+ Normalized_Fraction
+ Field_as_Ring
begin
subsection \<open>Various facts about polynomials\<close>
--- a/src/HOL/Library/Stream.thy Mon Apr 03 23:31:31 2017 +0200
+++ b/src/HOL/Library/Stream.thy Tue Apr 04 11:52:28 2017 +0200
@@ -9,7 +9,7 @@
section \<open>Infinite Streams\<close>
theory Stream
-imports "~~/src/HOL/Library/Nat_Bijection"
+ imports Nat_Bijection
begin
codatatype (sset: 'a) stream =