# HG changeset patch
# User blanchet
# Date 1502097671 -7200
# Node ID fa3247e6ee4bca7f5eccc4b97e611fc716643c07
# Parent  8aca34dbe195137d889ec5319eecfcf89dc6a882
tuning imports

diff -r 8aca34dbe195 -r fa3247e6ee4b src/HOL/ATP.thy
--- 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>
diff -r 8aca34dbe195 -r fa3247e6ee4b src/HOL/Equiv_Relations.thy
--- 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>
diff -r 8aca34dbe195 -r fa3247e6ee4b src/HOL/Groups_Big.thy
--- 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>
diff -r 8aca34dbe195 -r fa3247e6ee4b src/HOL/Lattices_Big.thy
--- 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>
diff -r 8aca34dbe195 -r fa3247e6ee4b src/HOL/Option.thy
--- 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 =
diff -r 8aca34dbe195 -r fa3247e6ee4b src/HOL/Partial_Function.thy
--- 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"