tuning imports
authorblanchet
Mon Aug 07 11:21:11 2017 +0200 (2017-08-07)
changeset 66364fa3247e6ee4b
parent 66363 8aca34dbe195
child 66366 e2f426b54922
tuning imports
src/HOL/ATP.thy
src/HOL/Equiv_Relations.thy
src/HOL/Groups_Big.thy
src/HOL/Lattices_Big.thy
src/HOL/Option.thy
src/HOL/Partial_Function.thy
     1.1 --- a/src/HOL/ATP.thy	Mon Aug 07 11:21:07 2017 +0200
     1.2 +++ b/src/HOL/ATP.thy	Mon Aug 07 11:21:11 2017 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  section \<open>Automatic Theorem Provers (ATPs)\<close>
     1.5  
     1.6  theory ATP
     1.7 -imports Meson
     1.8 +  imports Meson
     1.9  begin
    1.10  
    1.11  subsection \<open>ATP problems and proofs\<close>
     2.1 --- a/src/HOL/Equiv_Relations.thy	Mon Aug 07 11:21:07 2017 +0200
     2.2 +++ b/src/HOL/Equiv_Relations.thy	Mon Aug 07 11:21:11 2017 +0200
     2.3 @@ -5,7 +5,7 @@
     2.4  section \<open>Equivalence Relations in Higher-Order Set Theory\<close>
     2.5  
     2.6  theory Equiv_Relations
     2.7 -  imports Groups_Big Relation
     2.8 +  imports Groups_Big
     2.9  begin
    2.10  
    2.11  subsection \<open>Equivalence relations -- set version\<close>
     3.1 --- a/src/HOL/Groups_Big.thy	Mon Aug 07 11:21:07 2017 +0200
     3.2 +++ b/src/HOL/Groups_Big.thy	Mon Aug 07 11:21:11 2017 +0200
     3.3 @@ -8,7 +8,7 @@
     3.4  section \<open>Big sum and product over finite (non-empty) sets\<close>
     3.5  
     3.6  theory Groups_Big
     3.7 -  imports Finite_Set Power
     3.8 +  imports Power
     3.9  begin
    3.10  
    3.11  subsection \<open>Generic monoid operation over a set\<close>
     4.1 --- a/src/HOL/Lattices_Big.thy	Mon Aug 07 11:21:07 2017 +0200
     4.2 +++ b/src/HOL/Lattices_Big.thy	Mon Aug 07 11:21:11 2017 +0200
     4.3 @@ -6,7 +6,7 @@
     4.4  section \<open>Big infimum (minimum) and supremum (maximum) over finite (non-empty) sets\<close>
     4.5  
     4.6  theory Lattices_Big
     4.7 -imports Finite_Set Option
     4.8 +  imports Option
     4.9  begin
    4.10  
    4.11  subsection \<open>Generic lattice operations over a set\<close>
     5.1 --- a/src/HOL/Option.thy	Mon Aug 07 11:21:07 2017 +0200
     5.2 +++ b/src/HOL/Option.thy	Mon Aug 07 11:21:11 2017 +0200
     5.3 @@ -5,7 +5,7 @@
     5.4  section \<open>Datatype option\<close>
     5.5  
     5.6  theory Option
     5.7 -imports Lifting Finite_Set
     5.8 +  imports Lifting
     5.9  begin
    5.10  
    5.11  datatype 'a option =
     6.1 --- a/src/HOL/Partial_Function.thy	Mon Aug 07 11:21:07 2017 +0200
     6.2 +++ b/src/HOL/Partial_Function.thy	Mon Aug 07 11:21:11 2017 +0200
     6.3 @@ -5,8 +5,8 @@
     6.4  section \<open>Partial Function Definitions\<close>
     6.5  
     6.6  theory Partial_Function
     6.7 -imports Complete_Partial_Order Fun_Def_Base Option
     6.8 -keywords "partial_function" :: thy_decl
     6.9 +  imports Complete_Partial_Order Option
    6.10 +  keywords "partial_function" :: thy_decl
    6.11  begin
    6.12  
    6.13  named_theorems partial_function_mono "monotonicity rules for partial function definitions"