src/HOL/Ln.thy
changeset 39134 917b4b6ba3d2
parent 36777 be5461582d0f
child 40864 4abaaadfdaf2