src/HOL/Import/HOL4Compat.thy
changeset 28755 d5c1b7d67ea9
parent 23389 aaca6a8e5414
child 29044 45dfd04a972e