src/HOL/HOL.thy
changeset 6811 4700ca722bbd
parent 6795 35f214e73668
child 7127 48e235179ffb