--- 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 *}
--- 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"
--- 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 *}
--- 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 =
--- 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
--- 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
--- 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 *}