src/HOL/Real_Asymp/multiseries_expansion_bounds.ML
changeset 75575 06f8b072f28e
parent 69597 ff784d5a5bfb