src/HOL/ex/MT.thy
changeset 17184 3d80209e9a53
parent 15450 43dfc914d1b8
child 17289 8608f7a881eb