doc-src/TutorialI/Recdef/examples.thy
changeset 33776 5048b02c2bbb
parent 16417 9bc16273c2d4
equal deleted inserted replaced
33775:7a1518c42c56 33776:5048b02c2bbb