src/HOL/ex/MT.ML
changeset 9195 29f1e53f9937
parent 8114 09a7a180cc99
child 10202 9e8b4bebc940