--- a/src/HOL/Library/Library.thy Fri Feb 19 12:25:57 2016 +0100 +++ b/src/HOL/Library/Library.thy Tue Feb 09 09:21:10 2016 +0100 @@ -20,6 +20,7 @@ Dlist Extended Extended_Nat + Extended_Nonnegative_Real Extended_Real FinFun Float