doc-src/TutorialI/Recdef/examples.thy
changeset 29971 68331b62c873
parent 16417 9bc16273c2d4
equal deleted inserted replaced
29970:cbf46080ea3a 29971:68331b62c873