diff -r 163b265d3d83 -r ad39ca9477d5 src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Wed Dec 06 20:45:08 2000 +0100 +++ b/src/HOL/Library/Library.thy Wed Dec 06 20:45:36 2000 +0100 @@ -1,8 +1,9 @@ (*<*) theory Library = - List_Prefix + Quotient + Ring_and_Field + + Rational_Numbers + + List_Prefix + Accessible_Part + Multiset + While_Combinator + While_Combinator_Example: