| changeset 10654 | 458068404143 |
| parent 10212 | 33fe2d701ddd |
| child 10885 | 90695f46440b |
--- a/doc-src/TutorialI/Recdef/Nested2.thy Wed Dec 13 09:32:55 2000 +0100 +++ b/doc-src/TutorialI/Recdef/Nested2.thy Wed Dec 13 09:39:53 2000 +0100 @@ -80,7 +80,7 @@ text{*\noindent or declare them globally -by giving them the @{text recdef_cong} attribute as in +by giving them the \isaindexbold{recdef_cong} attribute as in *} declare map_cong[recdef_cong];