src/HOL/HOL.thy
changeset 62825 e6e80a8bf624
parent 62522 d32c23d29968
child 62913 13252110a6fe