replaced apply-style proof for instance Multiset :: plus_ac0 by recommended Isar proof style
(*<*)
theory Library =
Accessible_Part +
Continuity +
FuncSet +
List_Prefix +
Multiset +
NatPair +
Nat_Infinity +
Nested_Environment +
Permutation +
Primes +
Quotient +
While_Combinator +
Word +
Zorn:
end
(*>*)