# HG changeset patch
# User wenzelm
# Date 1364324522 -3600
# Node ID 738598beeb267c3fa04b33512b46e95a459a8131
# Parent  e7b6b61b7be28d808d72d38fa29c4bbf47507627
tuned imports;

diff -r e7b6b61b7be2 -r 738598beeb26 src/HOL/Library/Code_Char.thy
--- a/src/HOL/Library/Code_Char.thy	Tue Mar 26 19:43:31 2013 +0100
+++ b/src/HOL/Library/Code_Char.thy	Tue Mar 26 20:02:02 2013 +0100
@@ -5,7 +5,7 @@
 header {* Code generation of pretty characters (and strings) *}
 
 theory Code_Char
-imports Main "~~/src/HOL/Library/Char_ord"
+imports Main Char_ord
 begin
 
 code_type char
diff -r e7b6b61b7be2 -r 738598beeb26 src/HOL/Library/Code_Real_Approx_By_Float.thy
--- a/src/HOL/Library/Code_Real_Approx_By_Float.thy	Tue Mar 26 19:43:31 2013 +0100
+++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy	Tue Mar 26 20:02:02 2013 +0100
@@ -1,7 +1,7 @@
 (* Authors: Florian Haftmann, Johannes Hölzl, Tobias Nipkow *)
 
 theory Code_Real_Approx_By_Float
-imports Complex_Main "~~/src/HOL/Library/Code_Target_Int"
+imports Complex_Main Code_Target_Int
 begin
 
 text{* \textbf{WARNING} This theory implements mathematical reals by machine
diff -r e7b6b61b7be2 -r 738598beeb26 src/HOL/Library/Countable_Set.thy
--- a/src/HOL/Library/Countable_Set.thy	Tue Mar 26 19:43:31 2013 +0100
+++ b/src/HOL/Library/Countable_Set.thy	Tue Mar 26 20:02:02 2013 +0100
@@ -6,7 +6,7 @@
 header {* Countable sets *}
 
 theory Countable_Set
-  imports "~~/src/HOL/Library/Countable" "~~/src/HOL/Library/Infinite_Set"
+imports Countable Infinite_Set
 begin
 
 subsection {* Predicate for countable sets *}
diff -r e7b6b61b7be2 -r 738598beeb26 src/HOL/Library/FinFun_Syntax.thy
--- a/src/HOL/Library/FinFun_Syntax.thy	Tue Mar 26 19:43:31 2013 +0100
+++ b/src/HOL/Library/FinFun_Syntax.thy	Tue Mar 26 20:02:02 2013 +0100
@@ -2,7 +2,9 @@
 
 header {* Pretty syntax for almost everywhere constant functions *}
 
-theory FinFun_Syntax imports FinFun begin
+theory FinFun_Syntax
+imports FinFun
+begin
 
 type_notation
   finfun ("(_ =>f /_)" [22, 21] 21)
diff -r e7b6b61b7be2 -r 738598beeb26 src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Tue Mar 26 19:43:31 2013 +0100
+++ b/src/HOL/Library/Float.thy	Tue Mar 26 20:02:02 2013 +0100
@@ -6,7 +6,7 @@
 header {* Floating-Point Numbers *}
 
 theory Float
-imports Complex_Main "~~/src/HOL/Library/Lattice_Algebras"
+imports Complex_Main Lattice_Algebras
 begin
 
 definition "float = {m * 2 powr e | (m :: int) (e :: int). True}"
diff -r e7b6b61b7be2 -r 738598beeb26 src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Tue Mar 26 19:43:31 2013 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy	Tue Mar 26 20:02:02 2013 +0100
@@ -5,7 +5,7 @@
 header{* A formalization of formal power series *}
 
 theory Formal_Power_Series
-imports Complex_Main Binomial
+imports Binomial
 begin
 
 
diff -r e7b6b61b7be2 -r 738598beeb26 src/HOL/Library/Function_Growth.thy
--- a/src/HOL/Library/Function_Growth.thy	Tue Mar 26 19:43:31 2013 +0100
+++ b/src/HOL/Library/Function_Growth.thy	Tue Mar 26 20:02:02 2013 +0100
@@ -4,7 +4,7 @@
 header {* Comparing growth of functions on natural numbers by a preorder relation *}
 
 theory Function_Growth
-imports Main "~~/src/HOL/Library/Preorder" "~~/src/HOL/Library/Discrete"
+imports Main Preorder Discrete
 begin
 
 subsection {* Motivation *}
diff -r e7b6b61b7be2 -r 738598beeb26 src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Tue Mar 26 19:43:31 2013 +0100
+++ b/src/HOL/Library/Library.thy	Tue Mar 26 20:02:02 2013 +0100
@@ -16,7 +16,9 @@
   Debug
   Diagonal_Subsequence
   Dlist
-  Extended Extended_Nat Extended_Real
+  Extended
+  Extended_Nat
+  Extended_Real
   FinFun
   Float
   Formal_Power_Series
diff -r e7b6b61b7be2 -r 738598beeb26 src/HOL/Library/Liminf_Limsup.thy
--- a/src/HOL/Library/Liminf_Limsup.thy	Tue Mar 26 19:43:31 2013 +0100
+++ b/src/HOL/Library/Liminf_Limsup.thy	Tue Mar 26 20:02:02 2013 +0100
@@ -5,7 +5,7 @@
 header {* Liminf and Limsup on complete lattices *}
 
 theory Liminf_Limsup
-imports "~~/src/HOL/Complex_Main"
+imports Complex_Main
 begin
 
 lemma le_Sup_iff_less:
diff -r e7b6b61b7be2 -r 738598beeb26 src/HOL/Library/Permutation.thy
--- a/src/HOL/Library/Permutation.thy	Tue Mar 26 19:43:31 2013 +0100
+++ b/src/HOL/Library/Permutation.thy	Tue Mar 26 20:02:02 2013 +0100
@@ -5,7 +5,7 @@
 header {* Permutations *}
 
 theory Permutation
-imports Main Multiset
+imports Multiset
 begin
 
 inductive
diff -r e7b6b61b7be2 -r 738598beeb26 src/HOL/Library/Phantom_Type.thy
--- a/src/HOL/Library/Phantom_Type.thy	Tue Mar 26 19:43:31 2013 +0100
+++ b/src/HOL/Library/Phantom_Type.thy	Tue Mar 26 20:02:02 2013 +0100
@@ -4,7 +4,9 @@
 
 header {* A generic phantom type *}
 
-theory Phantom_Type imports Main begin
+theory Phantom_Type
+imports Main
+begin
 
 datatype ('a, 'b) phantom = phantom 'b
 
diff -r e7b6b61b7be2 -r 738598beeb26 src/HOL/Library/Product_Order.thy
--- a/src/HOL/Library/Product_Order.thy	Tue Mar 26 19:43:31 2013 +0100
+++ b/src/HOL/Library/Product_Order.thy	Tue Mar 26 20:02:02 2013 +0100
@@ -5,7 +5,7 @@
 header {* Pointwise order on product types *}
 
 theory Product_Order
-imports "~~/src/HOL/Library/Product_plus"
+imports Product_plus
 begin
 
 subsection {* Pointwise ordering *}
diff -r e7b6b61b7be2 -r 738598beeb26 src/HOL/Library/Reflection.thy
--- a/src/HOL/Library/Reflection.thy	Tue Mar 26 19:43:31 2013 +0100
+++ b/src/HOL/Library/Reflection.thy	Tue Mar 26 20:02:02 2013 +0100
@@ -8,8 +8,8 @@
 imports Main
 begin
 
-ML_file "~~/src/HOL/Library/reify_data.ML"
-ML_file "~~/src/HOL/Library/reflection.ML"
+ML_file "reify_data.ML"
+ML_file "reflection.ML"
 
 setup {* Reify_Data.setup *}
 
diff -r e7b6b61b7be2 -r 738598beeb26 src/HOL/Library/Saturated.thy
--- a/src/HOL/Library/Saturated.thy	Tue Mar 26 19:43:31 2013 +0100
+++ b/src/HOL/Library/Saturated.thy	Tue Mar 26 20:02:02 2013 +0100
@@ -7,7 +7,7 @@
 header {* Saturated arithmetic *}
 
 theory Saturated
-imports Main "~~/src/HOL/Library/Numeral_Type" "~~/src/HOL/Word/Type_Length"
+imports Numeral_Type "~~/src/HOL/Word/Type_Length"
 begin
 
 subsection {* The type of saturated naturals *}