doc-src/TutorialI/Recdef/document/Nested2.tex
changeset 10171 59d6633835fa
parent 9940 102f2430cef9
child 10212 33fe2d701ddd
     1.1 --- a/doc-src/TutorialI/Recdef/document/Nested2.tex	Mon Oct 09 09:33:45 2000 +0200
     1.2 +++ b/doc-src/TutorialI/Recdef/document/Nested2.tex	Mon Oct 09 10:18:21 2000 +0200
     1.3 @@ -72,7 +72,7 @@
     1.4  rules, you can either append a hint locally
     1.5  to the specific occurrence of \isacommand{recdef}%
     1.6  \end{isamarkuptext}%
     1.7 -{\isacharparenleft}\isakeyword{hints}\ cong{\isacharcolon}\ map{\isacharunderscore}cong{\isacharparenright}%
     1.8 +{\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}cong{\isacharcolon}\ map{\isacharunderscore}cong{\isacharparenright}%
     1.9  \begin{isamarkuptext}%
    1.10  \noindent
    1.11  or declare them globally
    1.12 @@ -80,10 +80,11 @@
    1.13  \end{isamarkuptext}%
    1.14  \isacommand{declare}\ map{\isacharunderscore}cong{\isacharbrackleft}recdef{\isacharunderscore}cong{\isacharbrackright}%
    1.15  \begin{isamarkuptext}%
    1.16 -Note that the global \isa{cong} and \isa{recdef{\isacharunderscore}cong} attributes are
    1.17 +Note that the \isa{cong} and \isa{recdef{\isacharunderscore}cong} attributes are
    1.18  intentionally kept apart because they control different activities, namely
    1.19 -simplification and making recursive definitions. The local \isa{cong} in
    1.20 -the hints section of \isacommand{recdef} is merely short for \isa{recdef{\isacharunderscore}cong}.
    1.21 +simplification and making recursive definitions.
    1.22 +% The local \isa{cong} in
    1.23 +% the hints section of \isacommand{recdef} is merely short for \isa{recdef{\isacharunderscore}cong}.
    1.24  %The simplifier's congruence rules cannot be used by recdef.
    1.25  %For example the weak congruence rules for if and case would prevent
    1.26  %recdef from generating sensible termination conditions.%