src/HOL/Hyperreal/Ln.thy
changeset 25343 31c55418de5a
parent 23482 2f4be6844f7c
child 25875 536dfdc25e0a