doc-src/TutorialI/Recdef/Nested2.thy
changeset 10121 fb9be005cc44
parent 9940 102f2430cef9
child 10171 59d6633835fa