src/Doc/Tutorial/Recdef/Nested1.thy
changeset 53683 e6adad558def
parent 48985 5386df44a037
child 56846 9df717fef2bb