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
     1

     2 % $Id$

     3

     4 \input{style}

     5

     6 \hyphenation{Isabelle}

     7

     8 \begin{document}

     9

    10 \title{Miscellaneous Isabelle/Isar examples for Higher-Order Logic}

    11 \author{Markus Wenzel \\ \url{http://www.in.tum.de/~wenzelm/} \\[2ex]

    12   With contributions by Gertrud Bauer and Tobias Nipkow}

    13 \maketitle

    14

    15 \begin{abstract}

    16   Isar offers a high-level proof (and theory) language for Isabelle.

    17   We give various examples of Isabelle/Isar proof developments,

    18   ranging from simple demonstrations of certain language features to

    19   more advanced applications.

    20 \end{abstract}

    21

    22 \tableofcontents

    23

    24 \parindent 0pt \parskip 0.5ex

    25

    26 \input{BasicLogic.tex}

    27 \input{Cantor.tex}

    28 \input{Peirce.tex}

    29 \input{ExprCompiler.tex}

    30 \input{Group.tex}

    31 \input{Summation.tex}

    32 \input{KnasterTarski.tex}

    33 \input{MutilatedCheckerboard.tex}

    34 %\input{Maybe.tex}

    35 %\input{Type.tex}

    36 \input{W_correct.tex}

    37 %\input{Primes.tex}

    38 \input{Fibonacci.tex}

    39 \input{Puzzle.tex}

    40 \input{NestedDatatype.tex}

    41 \input{Hoare.tex}

    42 \input{HoareEx.tex}

    43

    44 \nocite{isabelle-isar-ref,Wenzel:1999:TPHOL}

    45 \bibliographystyle{plain}

    46 \bibliography{root}

    47

    48 \end{document}