src/HOL/ex/MT.thy
changeset 15618 05bad476e0f0
parent 15450 43dfc914d1b8
child 17289 8608f7a881eb