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