src/HOL/HOL.thy
changeset 32538 86035c5f61b5
parent 32402 5731300da417
child 32544 e129333b9df0