src/HOL/Import/HOL4Compat.thy
changeset 29270 0eade173f77e
parent 29044 45dfd04a972e
child 30235 58d147683393