wneuper/isa: doc-src/IsarRef/isar-ref.tex@aad88e7344f0

     2 %% $Id$

     4 \documentclass[12pt,a4paper,fleqn]{report}

     5 \usepackage{latexsym,graphicx}

     6 \usepackage{../iman,../extra,../isar,../proof}

     7 \usepackage[nohyphen,strings]{../underscore}

     8 \usepackage{../isabelle,../isabellesym}

     9 \usepackage{../ttbox,,../rail,../railsetup}

    10 \usepackage{style}

    11 \usepackage{../pdfsetup}

    13 \hyphenation{Isabelle}

    14 \hyphenation{Isar}

    16 \isadroptag{theory}

    17 \title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] The Isabelle/Isar Reference Manual}

    18 \author{\emph{Makarius Wenzel} \\[3ex]

    19   With Contributions by

    20   Clemens Ballarin,

    21   Stefan Berghofer, \\

    22   Lucas Dixon,

    23   Florian Haftmann,

    24   Gerwin Klein, \\

    25   Alexander Krauss,

    26   Tobias Nipkow,

    27   David von Oheimb, \\

    28   Larry Paulson,

    29   and Sebastian Skalberg

    30 }

    32 \makeindex

    34 \railterm{percent,ppercent,underscore,lbrace,rbrace,atsign}

    35 \railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim,keyword}

    36 \railterm{name,nameref,text,type,term,prop,atom}

    38 \railalias{ident}{\railtok{ident}}

    39 \railalias{longident}{\railtok{longident}}

    40 \railalias{symident}{\railtok{symident}}

    41 \railalias{var}{\railtok{var}}

    42 \railalias{textvar}{\railtok{textvar}}

    43 \railalias{typefree}{\railtok{typefree}}

    44 \railalias{typevar}{\railtok{typevar}}

    45 \railalias{nat}{\railtok{nat}}

    46 \railalias{string}{\railtok{string}}

    47 \railalias{verbatim}{\railtok{verbatim}}

    48 \railalias{keyword}{\railtok{keyword}}

    50 \railalias{name}{\railqtok{name}}

    51 \railalias{nameref}{\railqtok{nameref}}

    52 \railalias{text}{\railqtok{text}}

    53 \railalias{type}{\railqtok{type}}

    54 \railalias{term}{\railqtok{term}}

    55 \railalias{prop}{\railqtok{prop}}

    56 \railalias{atom}{\railqtok{atom}}

    58 \railalias{subseteq}{\isasymsubseteq}\railterm{subseteq}

    59 \railalias{equiv}{\isasymequiv}\railterm{equiv}

    60 \railalias{rightleftharpoons}{\isasymrightleftharpoons}\railterm{rightleftharpoons}

    61 \railalias{rightharpoonup}{\isasymrightharpoonup}\railterm{rightharpoonup}

    62 \railalias{leftharpoondown}{\isasymleftharpoondown}\railterm{leftharpoondown}

    63 \railalias{verblbrace}{\texttt{\ttlbrace*}}\railterm{verblbrace}

    64 \railalias{verbrbrace}{\texttt{*\ttrbrace}}\railterm{verbrbrace}

    67 \chardef\charbackquote=`\`

    68 \newcommand{\backquote}{\mbox{\tt\charbackquote}}

    71 \begin{document}

    73 \maketitle

    75 \pagenumbering{roman} \tableofcontents \clearfirst

    77 \input{Thy/document/Introduction.tex}

    78 \input{Thy/document/Outer_Syntax.tex}

    79 \input{Thy/document/Document_Preparation.tex}

    80 \input{Thy/document/Spec.tex}

    81 \input{Thy/document/Proof.tex}

    82 \input{Thy/document/Misc.tex}

    83 \input{Thy/document/Generic.tex}

    84 \input{Thy/document/HOL_Specific.tex}

    85 \input{Thy/document/HOLCF_Specific.tex}

    86 \input{Thy/document/ZF_Specific.tex}

    88 \appendix

    89 \input{Thy/document/Quick_Reference.tex}

    90 \input{Thy/document/ML_Tactic.tex}

    92 \begingroup

    93   \bibliographystyle{plain} \small\raggedright\frenchspacing

    94   \bibliography{../manual}

    95 \endgroup

    97 \printindex

    99 \end{document}

author	wenzelm
	Thu, 13 Nov 2008 21:33:56 +0100
changeset 28751	aad88e7344f0
parent 27048	0e86aab627f3
child 28762	f5d79aeffd81
permissions	-rw-r--r--