doc-src/TutorialI/Recdef/Nested1.thy
changeset 11787 85b3735a51e1
parent 11636 0bec857c9871
child 12491 e28870d8b223