src/HOL/HOL.thy
changeset 71954 13bb3f5cdc5b
parent 71918 4e0a58818edc
child 71959 ee2c7f0dd1be