src/HOL/ex/MT.ML
changeset 23243 a37d3e6e8323
parent 22548 6ce4bddf3bcb