doc-src/TutorialI/Recdef/Nested1.thy
changeset 12124 c4fcdb80c93e
parent 11636 0bec857c9871
child 12491 e28870d8b223