# HG changeset patch
# User wenzelm
# Date 1001940167 -7200
# Node ID 6a7d80a139c6d918070a00e334a5af3df97ea7ef
# Parent  09a1876e739bf6378da8af84a63a8b7e328a6964
updated output;

diff -r 09a1876e739b -r 6a7d80a139c6 doc-src/TutorialI/fp.tex
--- a/doc-src/TutorialI/fp.tex	Mon Oct 01 13:39:17 2001 +0200
+++ b/doc-src/TutorialI/fp.tex	Mon Oct 01 14:42:47 2001 +0200
@@ -104,7 +104,7 @@
   \isa{rev(rev xs) = xs} is started, Isabelle prints the additional output
 \par\noindent
 \begin{isabelle}%
-Variables:\isanewline
+variables:\isanewline
 ~~xs~::~'a~list
 \end{isabelle}%
 \par\noindent
@@ -113,7 +113,7 @@
 made a typo as in \isa{rev(re xs) = xs}, the response
 \par\noindent
 \begin{isabelle}%
-Variables:\isanewline
+variables:\isanewline
 ~~re~::~'a~list~{\isasymRightarrow}~'a~list\isanewline
 ~~xs~::~'a~list%
 \end{isabelle}%