src/HOL/Ln.thy
changeset 49456 fa8302c8dea1
parent 47244 a7f85074c169
child 50326 b5afeccab2db