src/HOL/Ln.thy
changeset 33756 47b7c9e0bf6e
parent 33667 958dc9f03611
child 36777 be5461582d0f