src/HOL/HOL.thy
changeset 79037 1b3a6cc4a2bf
parent 78800 0b3700d31758
child 79772 817d33f8aa7f