doc-src/TutorialI/Recdef/Nested1.thy
changeset 15759 144c9f9a8ade
parent 12491 e28870d8b223
child 15905 0a4cc9b113c7
equal deleted inserted replaced
15758:07e382399a96 15759:144c9f9a8ade