src/HOL/Isar_examples/document/root.tex
author oheimb
Wed Jan 31 10:15:55 2001 +0100 (2001-01-31)
changeset 11008 f7333f055ef6
parent 10257 21055ac27708
child 12105 1e4451999200
permissions -rw-r--r--
improved theory reference in comment
wenzelm@9796
     1
wenzelm@9796
     2
% $Id$
wenzelm@7741
     3
wenzelm@7741
     4
\input{style}
wenzelm@7741
     5
wenzelm@7741
     6
\hyphenation{Isabelle}
wenzelm@7741
     7
wenzelm@7741
     8
\begin{document}
wenzelm@7741
     9
wenzelm@7741
    10
\title{Miscellaneous Isabelle/Isar examples for Higher-Order Logic}
wenzelm@8051
    11
\author{Markus Wenzel \\ \url{http://www.in.tum.de/~wenzelm/} \\[2ex]
wenzelm@8052
    12
  With contributions by Gertrud Bauer and Tobias Nipkow}
wenzelm@7741
    13
\maketitle
wenzelm@7741
    14
wenzelm@7741
    15
\begin{abstract}
wenzelm@7874
    16
  Isar offers a high-level proof (and theory) language for Isabelle.
wenzelm@7874
    17
  We give various examples of Isabelle/Isar proof developments,
wenzelm@7874
    18
  ranging from simple demonstrations of certain language features to
wenzelm@7874
    19
  more advanced applications.
wenzelm@7741
    20
\end{abstract}
wenzelm@7741
    21
wenzelm@7741
    22
\tableofcontents
wenzelm@7869
    23
wenzelm@7869
    24
\parindent 0pt \parskip 0.5ex
wenzelm@8189
    25
wenzelm@10146
    26
\input{BasicLogic.tex}
wenzelm@10146
    27
\input{Cantor.tex}
wenzelm@10146
    28
\input{Peirce.tex}
wenzelm@10146
    29
\input{ExprCompiler.tex}
wenzelm@10146
    30
\input{Group.tex}
wenzelm@10146
    31
\input{Summation.tex}
wenzelm@10146
    32
\input{KnasterTarski.tex}
wenzelm@10146
    33
\input{MutilatedCheckerboard.tex}
wenzelm@10146
    34
%\input{Maybe.tex}
wenzelm@10146
    35
%\input{Type.tex}
wenzelm@10146
    36
\input{W_correct.tex}
wenzelm@10146
    37
%\input{Primes.tex}
wenzelm@10146
    38
\input{Fibonacci.tex}
wenzelm@10146
    39
\input{Puzzle.tex}
wenzelm@10146
    40
\input{NestedDatatype.tex}
wenzelm@10146
    41
\input{Hoare.tex}
wenzelm@10146
    42
\input{HoareEx.tex}
wenzelm@7741
    43
wenzelm@7816
    44
\nocite{isabelle-isar-ref,Wenzel:1999:TPHOL}
wenzelm@7816
    45
\bibliographystyle{plain}
wenzelm@7816
    46
\bibliography{root}
wenzelm@7816
    47
wenzelm@7741
    48
\end{document}