# HG changeset patch
# User blanchet
# Date 1385066014 -3600
# Node ID e8c5e95d338b3bdf1877c14e49fb2efd1ec46bd0
# Parent  b8d0d8407c3bf8dc656024a2dc378e4fde54e0e4
rationalize imports

diff -r b8d0d8407c3b -r e8c5e95d338b src/HOL/Big_Operators.thy
--- a/src/HOL/Big_Operators.thy	Thu Nov 21 21:33:34 2013 +0100
+++ b/src/HOL/Big_Operators.thy	Thu Nov 21 21:33:34 2013 +0100
@@ -6,7 +6,7 @@
 header {* Big operators and finite (non-empty) sets *}
 
 theory Big_Operators
-imports Finite_Set Option Metis
+imports Finite_Set Metis
 begin
 
 subsection {* Generic monoid operation over a set *}
diff -r b8d0d8407c3b -r e8c5e95d338b src/HOL/Coinduction.thy
--- a/src/HOL/Coinduction.thy	Thu Nov 21 21:33:34 2013 +0100
+++ b/src/HOL/Coinduction.thy	Thu Nov 21 21:33:34 2013 +0100
@@ -9,7 +9,7 @@
 header {* Coinduction Method *}
 
 theory Coinduction
-imports Inductive
+imports Ctr_Sugar
 begin
 
 ML_file "Tools/coinduction.ML"
diff -r b8d0d8407c3b -r e8c5e95d338b src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Thu Nov 21 21:33:34 2013 +0100
+++ b/src/HOL/Lattices.thy	Thu Nov 21 21:33:34 2013 +0100
@@ -5,7 +5,7 @@
 header {* Abstract lattices *}
 
 theory Lattices
-imports Orderings Groups
+imports Groups
 begin
 
 subsection {* Abstract semilattice *}
diff -r b8d0d8407c3b -r e8c5e95d338b src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Nov 21 21:33:34 2013 +0100
+++ b/src/HOL/List.thy	Thu Nov 21 21:33:34 2013 +0100
@@ -5,7 +5,7 @@
 header {* The datatype of finite lists *}
 
 theory List
-imports Presburger Code_Numeral Quotient ATP Lifting_Set Lifting_Option Lifting_Product
+imports Presburger Code_Numeral Quotient Lifting_Set Lifting_Option Lifting_Product
 begin
 
 datatype 'a list =
diff -r b8d0d8407c3b -r e8c5e95d338b src/HOL/Nitpick.thy
--- a/src/HOL/Nitpick.thy	Thu Nov 21 21:33:34 2013 +0100
+++ b/src/HOL/Nitpick.thy	Thu Nov 21 21:33:34 2013 +0100
@@ -8,7 +8,7 @@
 header {* Nitpick: Yet Another Counterexample Generator for Isabelle/HOL *}
 
 theory Nitpick
-imports Hilbert_Choice List Map Quotient Record Sledgehammer
+imports Map Record Sledgehammer
 keywords "nitpick" :: diag and "nitpick_params" :: thy_decl
 begin
 
diff -r b8d0d8407c3b -r e8c5e95d338b src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Thu Nov 21 21:33:34 2013 +0100
+++ b/src/HOL/Quotient.thy	Thu Nov 21 21:33:34 2013 +0100
@@ -5,7 +5,7 @@
 header {* Definition of Quotient Types *}
 
 theory Quotient
-imports Hilbert_Choice Equiv_Relations Lifting
+imports Lifting
 keywords
   "print_quotmapsQ3" "print_quotientsQ3" "print_quotconsts" :: diag and
   "quotient_type" :: thy_goal and "/" and
diff -r b8d0d8407c3b -r e8c5e95d338b src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Thu Nov 21 21:33:34 2013 +0100
+++ b/src/HOL/Relation.thy	Thu Nov 21 21:33:34 2013 +0100
@@ -5,7 +5,7 @@
 header {* Relations – as sets of pairs, and binary predicates *}
 
 theory Relation
-imports Datatype Finite_Set
+imports Finite_Set
 begin
 
 text {* A preliminary: classical rules for reasoning on predicates *}