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