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