*** empty log message ***

--- 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: