src/HOL/ex/MT.ML
changeset 18583 96e1ef2f806f
parent 17778 93d7e524417a
child 20943 cf19faf11bbd