src/HOL/Isar_Examples/document/root.tex
changeset 61932 2e48182cc82c
parent 61542 b3eb789616c3
child 61935 6512e84cc9f5
equal deleted inserted replaced
61931:ed47044ee6a6 61932:2e48182cc82c
    14 \hyphenation{Isabelle}
    14 \hyphenation{Isabelle}
    15 
    15 
    16 \begin{document}
    16 \begin{document}
    17 
    17 
    18 \title{Miscellaneous Isabelle/Isar examples for Higher-Order Logic}
    18 \title{Miscellaneous Isabelle/Isar examples for Higher-Order Logic}
    19 \author{Markus Wenzel \\[2ex]
    19 \author{Makarius Wenzel \\[2ex]
    20   With contributions by Gertrud Bauer and Tobias Nipkow}
    20   With contributions by Gertrud Bauer and Tobias Nipkow}
    21 \maketitle
    21 \maketitle
    22 
    22 
    23 \begin{abstract}
    23 \begin{abstract}
    24   Isar offers a high-level proof (and theory) language for Isabelle.
    24   Isar offers a high-level proof (and theory) language for Isabelle.