src/HOL/TPTP/mash_export.ML
changeset 49494 cbcccf2a0f6f
parent 48667 ac58317ef11f
child 50349 b79803ee14f3