src/HOL/ex/MT.ML
changeset 15965 f422f8283491
parent 15386 06757406d8cf
child 17289 8608f7a881eb