src/HOL/Ln.thy
changeset 42150 b0c0638c4aad
parent 41959 b460124855b8
child 43336 05aa7380f7fc