src/HOL/HOL.thy
changeset 54253 04cd231e2b9e
parent 53146 3a93bc5d3370
child 54742 7a86358a3c0b