--- a/src/HOL/Library/Library.thy Tue Aug 29 20:34:43 2017 +0100 +++ b/src/HOL/Library/Library.thy Wed Aug 30 18:01:27 2017 +0200 @@ -82,6 +82,7 @@ Tree_Multiset Tree_Real Type_Length + Uprod While_Combinator begin end