src/HOL/HOL.thy
changeset 80004 31ebb6be32b0
parent 79772 817d33f8aa7f
child 80088 5afbf04418ec