*** empty log message ***
authornipkow
Fri, 16 Feb 2001 08:10:28 +0100
changeset 11148 79aa2932b2d7
parent 11147 d848c6693185
child 11149 e258b536a137
*** empty log message ***
doc-src/TutorialI/Types/numerics.tex
--- 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: