tuned imports;
authorwenzelm
Tue Mar 26 20:02:02 2013 +0100 (2013-03-26)
changeset 51542738598beeb26
parent 51541 e7b6b61b7be2
child 51543 118f7cb0ee8e
tuned imports;
src/HOL/Library/Code_Char.thy
src/HOL/Library/Code_Real_Approx_By_Float.thy
src/HOL/Library/Countable_Set.thy
src/HOL/Library/FinFun_Syntax.thy
src/HOL/Library/Float.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/Library/Function_Growth.thy
src/HOL/Library/Library.thy
src/HOL/Library/Liminf_Limsup.thy
src/HOL/Library/Permutation.thy
src/HOL/Library/Phantom_Type.thy
src/HOL/Library/Product_Order.thy
src/HOL/Library/Reflection.thy
src/HOL/Library/Saturated.thy
     1.1 --- a/src/HOL/Library/Code_Char.thy	Tue Mar 26 19:43:31 2013 +0100
     1.2 +++ b/src/HOL/Library/Code_Char.thy	Tue Mar 26 20:02:02 2013 +0100
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Code generation of pretty characters (and strings) *}
     1.5  
     1.6  theory Code_Char
     1.7 -imports Main "~~/src/HOL/Library/Char_ord"
     1.8 +imports Main Char_ord
     1.9  begin
    1.10  
    1.11  code_type char
     2.1 --- a/src/HOL/Library/Code_Real_Approx_By_Float.thy	Tue Mar 26 19:43:31 2013 +0100
     2.2 +++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy	Tue Mar 26 20:02:02 2013 +0100
     2.3 @@ -1,7 +1,7 @@
     2.4  (* Authors: Florian Haftmann, Johannes Hölzl, Tobias Nipkow *)
     2.5  
     2.6  theory Code_Real_Approx_By_Float
     2.7 -imports Complex_Main "~~/src/HOL/Library/Code_Target_Int"
     2.8 +imports Complex_Main Code_Target_Int
     2.9  begin
    2.10  
    2.11  text{* \textbf{WARNING} This theory implements mathematical reals by machine
     3.1 --- a/src/HOL/Library/Countable_Set.thy	Tue Mar 26 19:43:31 2013 +0100
     3.2 +++ b/src/HOL/Library/Countable_Set.thy	Tue Mar 26 20:02:02 2013 +0100
     3.3 @@ -6,7 +6,7 @@
     3.4  header {* Countable sets *}
     3.5  
     3.6  theory Countable_Set
     3.7 -  imports "~~/src/HOL/Library/Countable" "~~/src/HOL/Library/Infinite_Set"
     3.8 +imports Countable Infinite_Set
     3.9  begin
    3.10  
    3.11  subsection {* Predicate for countable sets *}
     4.1 --- a/src/HOL/Library/FinFun_Syntax.thy	Tue Mar 26 19:43:31 2013 +0100
     4.2 +++ b/src/HOL/Library/FinFun_Syntax.thy	Tue Mar 26 20:02:02 2013 +0100
     4.3 @@ -2,7 +2,9 @@
     4.4  
     4.5  header {* Pretty syntax for almost everywhere constant functions *}
     4.6  
     4.7 -theory FinFun_Syntax imports FinFun begin
     4.8 +theory FinFun_Syntax
     4.9 +imports FinFun
    4.10 +begin
    4.11  
    4.12  type_notation
    4.13    finfun ("(_ =>f /_)" [22, 21] 21)
     5.1 --- a/src/HOL/Library/Float.thy	Tue Mar 26 19:43:31 2013 +0100
     5.2 +++ b/src/HOL/Library/Float.thy	Tue Mar 26 20:02:02 2013 +0100
     5.3 @@ -6,7 +6,7 @@
     5.4  header {* Floating-Point Numbers *}
     5.5  
     5.6  theory Float
     5.7 -imports Complex_Main "~~/src/HOL/Library/Lattice_Algebras"
     5.8 +imports Complex_Main Lattice_Algebras
     5.9  begin
    5.10  
    5.11  definition "float = {m * 2 powr e | (m :: int) (e :: int). True}"
     6.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Tue Mar 26 19:43:31 2013 +0100
     6.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Tue Mar 26 20:02:02 2013 +0100
     6.3 @@ -5,7 +5,7 @@
     6.4  header{* A formalization of formal power series *}
     6.5  
     6.6  theory Formal_Power_Series
     6.7 -imports Complex_Main Binomial
     6.8 +imports Binomial
     6.9  begin
    6.10  
    6.11  
     7.1 --- a/src/HOL/Library/Function_Growth.thy	Tue Mar 26 19:43:31 2013 +0100
     7.2 +++ b/src/HOL/Library/Function_Growth.thy	Tue Mar 26 20:02:02 2013 +0100
     7.3 @@ -4,7 +4,7 @@
     7.4  header {* Comparing growth of functions on natural numbers by a preorder relation *}
     7.5  
     7.6  theory Function_Growth
     7.7 -imports Main "~~/src/HOL/Library/Preorder" "~~/src/HOL/Library/Discrete"
     7.8 +imports Main Preorder Discrete
     7.9  begin
    7.10  
    7.11  subsection {* Motivation *}
     8.1 --- a/src/HOL/Library/Library.thy	Tue Mar 26 19:43:31 2013 +0100
     8.2 +++ b/src/HOL/Library/Library.thy	Tue Mar 26 20:02:02 2013 +0100
     8.3 @@ -16,7 +16,9 @@
     8.4    Debug
     8.5    Diagonal_Subsequence
     8.6    Dlist
     8.7 -  Extended Extended_Nat Extended_Real
     8.8 +  Extended
     8.9 +  Extended_Nat
    8.10 +  Extended_Real
    8.11    FinFun
    8.12    Float
    8.13    Formal_Power_Series
     9.1 --- a/src/HOL/Library/Liminf_Limsup.thy	Tue Mar 26 19:43:31 2013 +0100
     9.2 +++ b/src/HOL/Library/Liminf_Limsup.thy	Tue Mar 26 20:02:02 2013 +0100
     9.3 @@ -5,7 +5,7 @@
     9.4  header {* Liminf and Limsup on complete lattices *}
     9.5  
     9.6  theory Liminf_Limsup
     9.7 -imports "~~/src/HOL/Complex_Main"
     9.8 +imports Complex_Main
     9.9  begin
    9.10  
    9.11  lemma le_Sup_iff_less:
    10.1 --- a/src/HOL/Library/Permutation.thy	Tue Mar 26 19:43:31 2013 +0100
    10.2 +++ b/src/HOL/Library/Permutation.thy	Tue Mar 26 20:02:02 2013 +0100
    10.3 @@ -5,7 +5,7 @@
    10.4  header {* Permutations *}
    10.5  
    10.6  theory Permutation
    10.7 -imports Main Multiset
    10.8 +imports Multiset
    10.9  begin
   10.10  
   10.11  inductive
    11.1 --- a/src/HOL/Library/Phantom_Type.thy	Tue Mar 26 19:43:31 2013 +0100
    11.2 +++ b/src/HOL/Library/Phantom_Type.thy	Tue Mar 26 20:02:02 2013 +0100
    11.3 @@ -4,7 +4,9 @@
    11.4  
    11.5  header {* A generic phantom type *}
    11.6  
    11.7 -theory Phantom_Type imports Main begin
    11.8 +theory Phantom_Type
    11.9 +imports Main
   11.10 +begin
   11.11  
   11.12  datatype ('a, 'b) phantom = phantom 'b
   11.13  
    12.1 --- a/src/HOL/Library/Product_Order.thy	Tue Mar 26 19:43:31 2013 +0100
    12.2 +++ b/src/HOL/Library/Product_Order.thy	Tue Mar 26 20:02:02 2013 +0100
    12.3 @@ -5,7 +5,7 @@
    12.4  header {* Pointwise order on product types *}
    12.5  
    12.6  theory Product_Order
    12.7 -imports "~~/src/HOL/Library/Product_plus"
    12.8 +imports Product_plus
    12.9  begin
   12.10  
   12.11  subsection {* Pointwise ordering *}
    13.1 --- a/src/HOL/Library/Reflection.thy	Tue Mar 26 19:43:31 2013 +0100
    13.2 +++ b/src/HOL/Library/Reflection.thy	Tue Mar 26 20:02:02 2013 +0100
    13.3 @@ -8,8 +8,8 @@
    13.4  imports Main
    13.5  begin
    13.6  
    13.7 -ML_file "~~/src/HOL/Library/reify_data.ML"
    13.8 -ML_file "~~/src/HOL/Library/reflection.ML"
    13.9 +ML_file "reify_data.ML"
   13.10 +ML_file "reflection.ML"
   13.11  
   13.12  setup {* Reify_Data.setup *}
   13.13  
    14.1 --- a/src/HOL/Library/Saturated.thy	Tue Mar 26 19:43:31 2013 +0100
    14.2 +++ b/src/HOL/Library/Saturated.thy	Tue Mar 26 20:02:02 2013 +0100
    14.3 @@ -7,7 +7,7 @@
    14.4  header {* Saturated arithmetic *}
    14.5  
    14.6  theory Saturated
    14.7 -imports Main "~~/src/HOL/Library/Numeral_Type" "~~/src/HOL/Word/Type_Length"
    14.8 +imports Numeral_Type "~~/src/HOL/Word/Type_Length"
    14.9  begin
   14.10  
   14.11  subsection {* The type of saturated naturals *}