# HG changeset patch
# User wenzelm
# Date 1491299548 -7200
# Node ID 10ca63a18e56c537449eb42df916742feb497ff9
# Parent  d32e702d7ab8e850f9668b0ad8ea77f9859913ec
proper imports;
tuned headers;

diff -r d32e702d7ab8 -r 10ca63a18e56 src/HOL/Library/Combine_PER.thy
--- 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"
diff -r d32e702d7ab8 -r 10ca63a18e56 src/HOL/Library/Complete_Partial_Order2.thy
--- 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]:
diff -r d32e702d7ab8 -r 10ca63a18e56 src/HOL/Library/Extended.thy
--- 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>")
diff -r d32e702d7ab8 -r 10ca63a18e56 src/HOL/Library/Multiset_Permutations.thy
--- 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 *)
diff -r d32e702d7ab8 -r 10ca63a18e56 src/HOL/Library/Normalized_Fraction.thy
--- 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
diff -r d32e702d7ab8 -r 10ca63a18e56 src/HOL/Library/Polynomial.thy
--- 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>
diff -r d32e702d7ab8 -r 10ca63a18e56 src/HOL/Library/Polynomial_FPS.thy
--- 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
diff -r d32e702d7ab8 -r 10ca63a18e56 src/HOL/Library/Polynomial_Factorial.thy
--- 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>
diff -r d32e702d7ab8 -r 10ca63a18e56 src/HOL/Library/Stream.thy
--- 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 =