src/HOL/Import/HOL4Compat.thy
changeset 15130 dc6be28d7f4e
parent 15003 6145dd7538d7
child 16417 9bc16273c2d4