src/HOL/HOL.thy
changeset 29835 62da280e5d0b
parent 29608 564ea783ace8
child 29863 dadad1831e9d