src/HOL/Real_Asymp/real_asymp.ML
changeset 76445 4a3a105ecbcc
parent 74560 5c8177fd1295
child 80636 4041e7c8059d