changeset 11428 | 332347b9b942 |
parent 11277 | a2bff98d6e5d |
child 11494 | 23a118849801 |
11427:3ed58bbcf4bd | 11428:332347b9b942 |
---|---|
75 (*>*) |
75 (*>*) |
76 (hints recdef_cong: map_cong) |
76 (hints recdef_cong: map_cong) |
77 |
77 |
78 text{*\noindent |
78 text{*\noindent |
79 or declare them globally |
79 or declare them globally |
80 by giving them the \isaindexbold{recdef_cong} attribute as in |
80 by giving them the \attrdx{recdef_cong} attribute as in |
81 *} |
81 *} |
82 |
82 |
83 declare map_cong[recdef_cong] |
83 declare map_cong[recdef_cong] |
84 |
84 |
85 text{* |
85 text{* |