# HG changeset patch
# User paulson
# Date 1113910501 -7200
# Node ID 949204e73081a9ff7f9a1df9d36d0e40ca765002
# Parent  08cc20626a0f6f949a92ec1258fa263de0f128b8
auto update

diff -r 08cc20626a0f -r 949204e73081 doc-src/TutorialI/Types/document/Numbers.tex
--- a/doc-src/TutorialI/Types/document/Numbers.tex	Tue Apr 19 13:34:50 2005 +0200
+++ b/doc-src/TutorialI/Types/document/Numbers.tex	Tue Apr 19 13:35:01 2005 +0200
@@ -317,11 +317,6 @@
 \isamarkuptrue%
 \isamarkupfalse%
 \isamarkuptrue%
-\isanewline
-\isamarkupfalse%
-\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isadigit{3}}{\isacharslash}{\isadigit{4}}{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}{\isadigit{1}}{\isadigit{0}}{\isacharcircum}{\isadigit{1}}{\isadigit{5}}{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ real{\isacharparenright}{\isachardoublequote}\isanewline
-\isamarkupfalse%
-\isamarkupfalse%
 \isamarkupfalse%
 %
 \begin{isamarkuptext}%