doc-src/TutorialI/Overview/RECDEF.thy
changeset 12899 7d5b690253ee
parent 12815 1f073030b97a
child 13238 a6cb18a25cbb