--- a/src/HOL/Library/Library.thy Thu Sep 15 19:31:17 2016 +0200 +++ b/src/HOL/Library/Library.thy Thu Sep 15 22:41:05 2016 +0200 @@ -26,6 +26,7 @@ Extended_Nonnegative_Real Extended_Real FinFun + Finite_Map Float Formal_Power_Series Fraction_Field