src/Pure/ex/Def_Examples.thy
changeset 80523 532156e8f15f
parent 74287 f79dfc7656ae