src/HOL/HOL.thy
changeset 32496 4ab00a2642c3
parent 32402 5731300da417
child 32544 e129333b9df0