doc-src/TutorialI/Types/numerics.tex
changeset 11148 79aa2932b2d7
parent 10983 59961d32b1ae
child 11161 166f7d87b37f
--- 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: