doc-src/TutorialI/Recdef/examples.thy
changeset 34119 ae92efb48784
parent 16417 9bc16273c2d4
equal deleted inserted replaced
34118:ee9f87e11400 34119:ae92efb48784