src/HOL/HOL.thy
changeset 13592 dfe0c7191125
parent 13553 855f6bae851e
child 13596 ee5f79b210c1