src/HOL/HOL.thy
changeset 77215 6cc3b131f761
parent 77172 816959264c32
child 78099 4d9349989d94