src/HOL/Hyperreal/Ln.thy
changeset 23719 ccd9cb15c062
parent 23482 2f4be6844f7c
child 25875 536dfdc25e0a