src/HOL/ex/MT.ML
changeset 7843 077d305615df
parent 7499 23e090051cb8
child 8114 09a7a180cc99