src/HOL/HOL.thy
changeset 70657 2bf1d0e57695
parent 70486 1dc3514c1719
child 70847 e62d5433bb47