src/HOL/ex/MT.ML
changeset 8145 cdd5386eb6fe
parent 8114 09a7a180cc99
child 10202 9e8b4bebc940