src/HOL/Library/Library.thy
changeset 10616 ad39ca9477d5
parent 10481 9efb2fd5399e
child 10618 5b96bc5fbec3
equal deleted inserted replaced
10615:163b265d3d83 10616:ad39ca9477d5
     1 (*<*)
     1 (*<*)
     2 theory Library =
     2 theory Library =
     3   List_Prefix +
       
     4   Quotient +
     3   Quotient +
     5   Ring_and_Field +
     4   Ring_and_Field +
       
     5   Rational_Numbers +
       
     6   List_Prefix +
     6   Accessible_Part +
     7   Accessible_Part +
     7   Multiset +
     8   Multiset +
     8   While_Combinator + While_Combinator_Example:
     9   While_Combinator + While_Combinator_Example:
     9 end
    10 end
    10 (*>*)
    11 (*>*)