# HG changeset patch
# User nipkow
# Date 982307428 -3600
# Node ID 79aa2932b2d715beaa92da1b51f7ceee5cec3572
# Parent  d848c669318533ec8306915eb39760d6cce369eb
*** empty log message ***

diff -r d848c6693185 -r 79aa2932b2d7 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: