src/HOL/Ln.thy
changeset 43139 9ed5d8ad8fa0
parent 41959 b460124855b8
child 43336 05aa7380f7fc