src/HOL/HOL.thy
changeset 70759 26837fd025a3
parent 70486 1dc3514c1719
child 70847 e62d5433bb47