src/HOL/ex/MT.thy
changeset 14141 d3916d9183d2
parent 12338 de0f4a63baa5
child 15450 43dfc914d1b8
equal deleted inserted replaced
14140:ca089b9d13c4 14141:d3916d9183d2