changeset 10616 | ad39ca9477d5 |
parent 10481 | 9efb2fd5399e |
child 10618 | 5b96bc5fbec3 |
--- 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: