src/HOL/Import/HOL4Compat.thy
changeset 31106 9a1178204dc0
parent 30660 53e1b1641f09
child 30952 7ab2716dd93b