changeset 66364 | fa3247e6ee4b |
parent 65965 | 088c79b40156 |
child 66425 | 8756322dc5de |
--- 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>