--- a/src/HOL/ATP.thy Mon Aug 07 11:21:07 2017 +0200
+++ b/src/HOL/ATP.thy Mon Aug 07 11:21:11 2017 +0200
@@ -6,7 +6,7 @@
section \<open>Automatic Theorem Provers (ATPs)\<close>
theory ATP
-imports Meson
+ imports Meson
begin
subsection \<open>ATP problems and proofs\<close>
--- a/src/HOL/Equiv_Relations.thy Mon Aug 07 11:21:07 2017 +0200
+++ b/src/HOL/Equiv_Relations.thy Mon Aug 07 11:21:11 2017 +0200
@@ -5,7 +5,7 @@
section \<open>Equivalence Relations in Higher-Order Set Theory\<close>
theory Equiv_Relations
- imports Groups_Big Relation
+ imports Groups_Big
begin
subsection \<open>Equivalence relations -- set version\<close>
--- a/src/HOL/Groups_Big.thy Mon Aug 07 11:21:07 2017 +0200
+++ b/src/HOL/Groups_Big.thy Mon Aug 07 11:21:11 2017 +0200
@@ -8,7 +8,7 @@
section \<open>Big sum and product over finite (non-empty) sets\<close>
theory Groups_Big
- imports Finite_Set Power
+ imports Power
begin
subsection \<open>Generic monoid operation over a set\<close>
--- a/src/HOL/Lattices_Big.thy Mon Aug 07 11:21:07 2017 +0200
+++ b/src/HOL/Lattices_Big.thy Mon Aug 07 11:21:11 2017 +0200
@@ -6,7 +6,7 @@
section \<open>Big infimum (minimum) and supremum (maximum) over finite (non-empty) sets\<close>
theory Lattices_Big
-imports Finite_Set Option
+ imports Option
begin
subsection \<open>Generic lattice operations over a set\<close>
--- a/src/HOL/Option.thy Mon Aug 07 11:21:07 2017 +0200
+++ b/src/HOL/Option.thy Mon Aug 07 11:21:11 2017 +0200
@@ -5,7 +5,7 @@
section \<open>Datatype option\<close>
theory Option
-imports Lifting Finite_Set
+ imports Lifting
begin
datatype 'a option =
--- a/src/HOL/Partial_Function.thy Mon Aug 07 11:21:07 2017 +0200
+++ b/src/HOL/Partial_Function.thy Mon Aug 07 11:21:11 2017 +0200
@@ -5,8 +5,8 @@
section \<open>Partial Function Definitions\<close>
theory Partial_Function
-imports Complete_Partial_Order Fun_Def_Base Option
-keywords "partial_function" :: thy_decl
+ imports Complete_Partial_Order Option
+ keywords "partial_function" :: thy_decl
begin
named_theorems partial_function_mono "monotonicity rules for partial function definitions"