src/HOL/TPTP/mash_export.ML
changeset 76371 1ac2416e8432
parent 76092 282f5e980a67
child 77889 5db014c36f42