doc-src/TutorialI/Overview/RECDEF.thy
changeset 13261 a0460a450cf9
parent 13249 4b3de6370184