src/HOL/ex/MT.ML
changeset 9811 39ffdb8cab03
parent 8114 09a7a180cc99
child 10202 9e8b4bebc940
equal deleted inserted replaced
9810:7e785df2b76a 9811:39ffdb8cab03