doc-src/TutorialI/Recdef/examples.thy
changeset 43620 43a195a0279b
parent 16417 9bc16273c2d4
equal deleted inserted replaced
43619:3803869014aa 43620:43a195a0279b