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}