author nipkow Thu, 15 Feb 2001 11:15:39 +0100 changeset 11129 6f6892bea902 parent 11128 48c63b87566e child 11130 d14fd58615b9
*** empty log message ***
--- a/doc-src/TutorialI/Inductive/even-example.tex	Thu Feb 15 00:53:45 2001 +0100
+++ b/doc-src/TutorialI/Inductive/even-example.tex	Thu Feb 15 11:15:39 2001 +0100
@@ -2,7 +2,7 @@
\section{The Set of Even Numbers}

The set of even numbers can be inductively defined as the least set
-containing 0 and closed under the operation ${\cdots}+2$.  Obviously,
+containing 0 and closed under the operation $+2$.  Obviously,
\emph{even} can also be expressed using the divides relation (\isa{dvd}).
We shall prove below that the two formulations coincide.  On the way we
shall examine the primary means of reasoning about inductively defined
@@ -73,7 +73,7 @@
Our ultimate goal is to prove the equivalence between the traditional
definition of \isa{even} (using the divides relation) and our inductive
definition.  One direction of this equivalence is immediate by the lemma
-just proved, whose \isa{intro!} attribute ensures it will be used.
+just proved, whose \isa{intro!} attribute ensures it is applied automatically.
\begin{isabelle}
\isacommand{lemma}\ dvd_imp_even:\ "\#2\ dvd\ n\ \isasymLongrightarrow \ n\ \isasymin \ even"\isanewline
-\isa{Suc(Suc$$\cdots$$)}.  Then \isa{P} is closed under the introduction
+\isa{Suc(Suc $$\cdot$$)}.  Then \isa{P} is closed under the introduction