src/HOL/Isar_examples/document/root.tex
changeset 7800 8ee919e42174
parent 7741 874abb8aa65b
child 7806 991d6c09930e
equal deleted inserted replaced
7799:4c69318e6a6d 7800:8ee919e42174
     1 
     1 
     2 \input{style}
     2 \input{style}
     3 
     3 
     4 \hyphenation{Isabelle}
     4 \hyphenation{Isabelle}
     5 
       
     6 
     5 
     7 \begin{document}
     6 \begin{document}
     8 
     7 
     9 \title{Miscellaneous Isabelle/Isar examples for Higher-Order Logic}
     8 \title{Miscellaneous Isabelle/Isar examples for Higher-Order Logic}
    10 \author{Markus Wenzel}
     9 \author{Markus Wenzel}
    16   simple demonstrations of certain language features to more advanced
    15   simple demonstrations of certain language features to more advanced
    17   applications.
    16   applications.
    18 \end{abstract}
    17 \end{abstract}
    19 
    18 
    20 \tableofcontents
    19 \tableofcontents
    21 
       
    22 \input{session}
    20 \input{session}
    23 
    21 
    24 \end{document}
    22 \end{document}