src/HOL/TPTP/mash_export.ML
changeset 65946 5dd3974cf0bc
parent 65458 cf504b7a7aa7
child 69597 ff784d5a5bfb