src/HOL/Real_Asymp/real_asymp.ML
changeset 79388 e6a12ea61f83
parent 74560 5c8177fd1295
child 80636 4041e7c8059d