src/HOL/HOL.thy
changeset 27090 2f45c1b1b05d
parent 26957 e3f04fdd994d
child 27107 4a7415c67063