src/HOL/Real_Asymp/exp_log_expression.ML
changeset 79388 e6a12ea61f83
parent 78095 bc42c074e58f
child 81946 ee680c69de38