src/HOL/Hyperreal/Ln.thy
changeset 22898 38ae2815989f
parent 22654 c2b6b5a9e136
child 22998 97e1f9c2cc46