src/HOL/Real_Asymp/asymptotic_basis.ML
changeset 70716 a8afe8eb3529
parent 69597 ff784d5a5bfb