src/HOL/ex/MT.thy
changeset 25517 36d710d1dbce
parent 24326 3e9d3ba894b8
child 41460 ea56b98aee83