--- a/src/HOL/Isar_examples/document/root.tex Wed Nov 16 17:50:35 2005 +0100
+++ b/src/HOL/Isar_examples/document/root.tex Wed Nov 16 19:34:19 2005 +0100
@@ -13,11 +13,11 @@
\maketitle
\begin{abstract}
- Isar offers a high-level proof (and theory) language for Isabelle. We give
- various examples of Isabelle/Isar proof developments, ranging from simple
- demonstrations of certain language features to a bit more advanced
- applications. Note that the ``real'' applications of Isar are found
- elsewhere.
+ Isar offers a high-level proof (and theory) language for Isabelle.
+ We give various examples of Isabelle/Isar proof developments,
+ ranging from simple demonstrations of certain language features to a
+ bit more advanced applications. The ``real'' applications of
+ Isabelle/Isar are found elsewhere.
\end{abstract}
\tableofcontents