doc-src/TutorialI/Recdef/Nested0.thy
changeset 11420 9529d31f39e0
parent 11196 bb4ede27fcb7
child 11494 23a118849801
equal deleted inserted replaced
11419:9577530e8a5a 11420:9529d31f39e0