--- a/doc-src/TutorialI/Misc/AdvancedInd.thy Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/Misc/AdvancedInd.thy Tue Sep 05 09:03:17 2000 +0200
@@ -135,9 +135,7 @@
usually known as ``mathematical induction''. There is also ``complete
induction'', where you must prove $P(n)$ under the assumption that $P(m)$
holds for all $m<n$. In Isabelle, this is the theorem @{thm[source]less_induct}:
-\begin{quote}
@{thm[display]"less_induct"[no_vars]}
-\end{quote}
Here is an example of its application.
*};
@@ -267,9 +265,7 @@
text{*\noindent
The elimination rule @{thm[source]less_SucE} expresses the case distinction:
-\begin{quote}
@{thm[display]"less_SucE"[no_vars]}
-\end{quote}
Now it is straightforward to derive the original version of
@{thm[source]less_induct} by manipulting the conclusion of the above lemma:
@@ -285,9 +281,7 @@
text{*\noindent
Finally we should mention that HOL already provides the mother of all
inductions, \emph{wellfounded induction} (@{thm[source]wf_induct}):
-\begin{quote}
@{thm[display]"wf_induct"[no_vars]}
-\end{quote}
where @{term"wf r"} means that the relation @{term"r"} is wellfounded.
For example @{thm[source]less_induct} is the special case where @{term"r"} is
@{text"<"} on @{typ"nat"}. For details see the library.