src/HOL/TPTP/mash_export.ML
changeset 50936 b28f258ebc1a
parent 50907 a86708897266
child 50954 7bc58677860e