src/HOL/Hyperreal/Ln.thy
changeset 27475 61b979a2c820
parent 25875 536dfdc25e0a
child 27483 7c58324cd418