--- a/src/HOL/Isar_examples/document/root.tex Thu Nov 08 17:54:58 2001 +0100
+++ b/src/HOL/Isar_examples/document/root.tex Thu Nov 08 23:50:08 2001 +0100
@@ -13,36 +13,21 @@
\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
- more advanced applications.
+ 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.
\end{abstract}
\tableofcontents
\parindent 0pt \parskip 0.5ex
-\input{BasicLogic.tex}
-\input{Cantor.tex}
-\input{Peirce.tex}
-\input{ExprCompiler.tex}
-\input{Group.tex}
-\input{Summation.tex}
-\input{KnasterTarski.tex}
-\input{MutilatedCheckerboard.tex}
-%\input{Maybe.tex}
-%\input{Type.tex}
-\input{W_correct.tex}
-%\input{Primes.tex}
-\input{Fibonacci.tex}
-\input{Puzzle.tex}
-\input{NestedDatatype.tex}
-\input{Hoare.tex}
-\input{HoareEx.tex}
+\input{session}
\nocite{isabelle-isar-ref,Wenzel:1999:TPHOL}
-\bibliographystyle{plain}
+\bibliographystyle{abbrv}
\bibliography{root}
\end{document}