# HG changeset patch
# User wenzelm
# Date 1011886669 -3600
# Node ID b5b15bbca582b08f63cd27fa14b00686430be70b
# Parent  50bd380e667517ec422f4caeaf0bfe5bf95b75e0
updated;

diff -r 50bd380e6675 -r b5b15bbca582 doc-src/TutorialI/Types/document/Numbers.tex
--- a/doc-src/TutorialI/Types/document/Numbers.tex	Thu Jan 24 16:37:43 2002 +0100
+++ b/doc-src/TutorialI/Types/document/Numbers.tex	Thu Jan 24 16:37:49 2002 +0100
@@ -132,7 +132,7 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}n\ {\isacharminus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharequal}\ n\ {\isacharasterisk}\ n\ {\isacharminus}\ {\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{apply}\ {\isacharparenleft}clarsimp\ split{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}\isanewline
+\isacommand{apply}\ {\isacharparenleft}clarsimp\ split{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split\ iff\ del{\isacharcolon}\ less{\isacharunderscore}Suc{\isadigit{0}}{\isacharparenright}\isanewline
 \ %
 \isamarkupcmt{\begin{isabelle}%
 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}d{\isachardot}\ {\isasymlbrakk}n\ {\isacharless}\ Suc\ {\isadigit{0}}{\isacharsemicolon}\ n\ {\isacharasterisk}\ n\ {\isacharequal}\ Suc\ d{\isasymrbrakk}\ {\isasymLongrightarrow}\ d\ {\isacharequal}\ {\isadigit{0}}%