src/HOL/HOL.thy
changeset 29795 c78806b621e1
parent 29608 564ea783ace8
child 29863 dadad1831e9d