src/Doc/Tutorial/Recdef/Nested1.thy
changeset 55424 9ab4129a76a3
parent 48985 5386df44a037
child 56846 9df717fef2bb
equal deleted inserted replaced
55423:07dea66779f3 55424:9ab4129a76a3