src/HOL/Ln.thy
changeset 50497 492953de3090
parent 50326 b5afeccab2db