src/HOL/HOL.thy
changeset 53946 5431e1392b14
parent 53146 3a93bc5d3370
child 54742 7a86358a3c0b