src/HOL/HOL.thy
changeset 9030 bb7622789bf2
parent 8959 9d793220a46a
child 9060 b0dd884b1848