src/HOL/ex/MT.ML
changeset 17184 3d80209e9a53
parent 15386 06757406d8cf
child 17289 8608f7a881eb