changeset 54555 | e8c5e95d338b |
parent 54230 | b1d955791529 |
--- 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 *}