src/HOL/Real_Asymp/asymptotic_basis.ML
changeset 79388 e6a12ea61f83
parent 69597 ff784d5a5bfb