src/HOL/Import/HOL4Compat.thy
changeset 30681 27ee3f4ea99c
parent 30660 53e1b1641f09
child 30952 7ab2716dd93b