doc-src/TutorialI/Recdef/Nested1.thy
changeset 12434 ff2efde4574d
parent 11636 0bec857c9871
child 12491 e28870d8b223
equal deleted inserted replaced
12433:654acbf26fcc 12434:ff2efde4574d