src/HOL/Import/HOL4Compat.thy
changeset 20192 956cd30ef3be
parent 19064 bf19cc5a7899
child 20269 c40070317ab8