src/HOL/HOL.thy
changeset 79517 0856026e2c88
parent 78800 0b3700d31758
child 79772 817d33f8aa7f