src/HOL/Real_Asymp/asymptotic_basis.ML
changeset 79268 154166613b40
parent 69597 ff784d5a5bfb