src/HOL/HOL.thy
changeset 7301 6d43d525facc
parent 7238 36e58620ffc8
child 7357 d0e16da40ea2