src/HOL/HOL.thy
changeset 82274 c61367ada9bb
parent 81954 6f2bcdfa9a19
child 82360 6a09257afd06