author | nipkow |
Fri, 16 Feb 2001 08:10:28 +0100 | |
changeset 11148 | 79aa2932b2d7 |
parent 11147 | d848c6693185 |
child 11149 | e258b536a137 |
--- a/doc-src/TutorialI/Types/numerics.tex Fri Feb 16 06:46:20 2001 +0100 +++ b/doc-src/TutorialI/Types/numerics.tex Fri Feb 16 08:10:28 2001 +0100 @@ -77,8 +77,8 @@ patterns. For example, this declaration is rejected: \begin{isabelle} \isacommand{recdef}\ h\ "\isacharbraceleft \isacharbraceright "\isanewline -h\ \#3\ =\ \#2\isanewline -h\ i\ \ =\ i +"h\ \#3\ =\ \#2"\isanewline +"h\ i\ \ =\ i" \end{isabelle} You should use a conditional expression instead: