src/HOL/Hyperreal/Ln.thy
changeset 26086 3c243098b64a
parent 25875 536dfdc25e0a
child 27483 7c58324cd418