| changeset 10654 | 458068404143 |
| parent 10212 | 33fe2d701ddd |
| child 10885 | 90695f46440b |
| 10653:55f33da63366 | 10654:458068404143 |
|---|---|
78 (*>*) |
78 (*>*) |
79 (hints recdef_cong: map_cong) |
79 (hints recdef_cong: map_cong) |
80 |
80 |
81 text{*\noindent |
81 text{*\noindent |
82 or declare them globally |
82 or declare them globally |
83 by giving them the @{text recdef_cong} attribute as in |
83 by giving them the \isaindexbold{recdef_cong} attribute as in |
84 *} |
84 *} |
85 |
85 |
86 declare map_cong[recdef_cong]; |
86 declare map_cong[recdef_cong]; |
87 |
87 |
88 text{* |
88 text{* |