doc-src/TutorialI/Recdef/examples.thy
changeset 36806 fc27b0465a4c
parent 16417 9bc16273c2d4
equal deleted inserted replaced
36805:929b23461a14 36806:fc27b0465a4c