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