src/HOL/Hyperreal/Ln.thy
changeset 20439 1bf42b262a38
parent 20432 07ec57376051
child 20563 44eda2314aab