(*<*) theory Library imports Accessible_Part BigO Continuity EfficientNat FuncSet Multiset NatPair Nat_Infinity Nested_Environment OptionalSugar Permutation Primes Quotient While_Combinator Word Zorn Char_ord begin end (*>*)