src/HOL/HOL.thy
changeset 78684 aa532cf1c894
parent 78099 4d9349989d94
child 78794 c74fd21af246