src/HOL/ex/MT.ML
changeset 21404 eb85850d3eb7
parent 21026 3b2821e0d541
child 21546 268b6bed0cc8