src/HOL/HOL.thy
changeset 78928 6c2c60b852e0
parent 78800 0b3700d31758
child 79772 817d33f8aa7f