src/HOL/Import/HOL4Compat.thy
changeset 21140 1c0805003c4f
parent 20432 07ec57376051
child 23389 aaca6a8e5414