src/HOL/TPTP/mash_export.ML
changeset 66787 64b47495676d
parent 65458 cf504b7a7aa7
child 69597 ff784d5a5bfb