rationalize imports
authorblanchet
Thu Nov 21 21:33:34 2013 +0100 (2013-11-21)
changeset 54555e8c5e95d338b
parent 54554 b8d0d8407c3b
child 54556 dd511ddcb203
rationalize imports
src/HOL/Big_Operators.thy
src/HOL/Coinduction.thy
src/HOL/Lattices.thy
src/HOL/List.thy
src/HOL/Nitpick.thy
src/HOL/Quotient.thy
src/HOL/Relation.thy
     1.1 --- a/src/HOL/Big_Operators.thy	Thu Nov 21 21:33:34 2013 +0100
     1.2 +++ b/src/HOL/Big_Operators.thy	Thu Nov 21 21:33:34 2013 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* Big operators and finite (non-empty) sets *}
     1.5  
     1.6  theory Big_Operators
     1.7 -imports Finite_Set Option Metis
     1.8 +imports Finite_Set Metis
     1.9  begin
    1.10  
    1.11  subsection {* Generic monoid operation over a set *}
     2.1 --- a/src/HOL/Coinduction.thy	Thu Nov 21 21:33:34 2013 +0100
     2.2 +++ b/src/HOL/Coinduction.thy	Thu Nov 21 21:33:34 2013 +0100
     2.3 @@ -9,7 +9,7 @@
     2.4  header {* Coinduction Method *}
     2.5  
     2.6  theory Coinduction
     2.7 -imports Inductive
     2.8 +imports Ctr_Sugar
     2.9  begin
    2.10  
    2.11  ML_file "Tools/coinduction.ML"
     3.1 --- a/src/HOL/Lattices.thy	Thu Nov 21 21:33:34 2013 +0100
     3.2 +++ b/src/HOL/Lattices.thy	Thu Nov 21 21:33:34 2013 +0100
     3.3 @@ -5,7 +5,7 @@
     3.4  header {* Abstract lattices *}
     3.5  
     3.6  theory Lattices
     3.7 -imports Orderings Groups
     3.8 +imports Groups
     3.9  begin
    3.10  
    3.11  subsection {* Abstract semilattice *}
     4.1 --- a/src/HOL/List.thy	Thu Nov 21 21:33:34 2013 +0100
     4.2 +++ b/src/HOL/List.thy	Thu Nov 21 21:33:34 2013 +0100
     4.3 @@ -5,7 +5,7 @@
     4.4  header {* The datatype of finite lists *}
     4.5  
     4.6  theory List
     4.7 -imports Presburger Code_Numeral Quotient ATP Lifting_Set Lifting_Option Lifting_Product
     4.8 +imports Presburger Code_Numeral Quotient Lifting_Set Lifting_Option Lifting_Product
     4.9  begin
    4.10  
    4.11  datatype 'a list =
     5.1 --- a/src/HOL/Nitpick.thy	Thu Nov 21 21:33:34 2013 +0100
     5.2 +++ b/src/HOL/Nitpick.thy	Thu Nov 21 21:33:34 2013 +0100
     5.3 @@ -8,7 +8,7 @@
     5.4  header {* Nitpick: Yet Another Counterexample Generator for Isabelle/HOL *}
     5.5  
     5.6  theory Nitpick
     5.7 -imports Hilbert_Choice List Map Quotient Record Sledgehammer
     5.8 +imports Map Record Sledgehammer
     5.9  keywords "nitpick" :: diag and "nitpick_params" :: thy_decl
    5.10  begin
    5.11  
     6.1 --- a/src/HOL/Quotient.thy	Thu Nov 21 21:33:34 2013 +0100
     6.2 +++ b/src/HOL/Quotient.thy	Thu Nov 21 21:33:34 2013 +0100
     6.3 @@ -5,7 +5,7 @@
     6.4  header {* Definition of Quotient Types *}
     6.5  
     6.6  theory Quotient
     6.7 -imports Hilbert_Choice Equiv_Relations Lifting
     6.8 +imports Lifting
     6.9  keywords
    6.10    "print_quotmapsQ3" "print_quotientsQ3" "print_quotconsts" :: diag and
    6.11    "quotient_type" :: thy_goal and "/" and
     7.1 --- a/src/HOL/Relation.thy	Thu Nov 21 21:33:34 2013 +0100
     7.2 +++ b/src/HOL/Relation.thy	Thu Nov 21 21:33:34 2013 +0100
     7.3 @@ -5,7 +5,7 @@
     7.4  header {* Relations – as sets of pairs, and binary predicates *}
     7.5  
     7.6  theory Relation
     7.7 -imports Datatype Finite_Set
     7.8 +imports Finite_Set
     7.9  begin
    7.10  
    7.11  text {* A preliminary: classical rules for reasoning on predicates *}