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

     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/Spec.tex}

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

    81 \input{Thy/document/Document_Preparation.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
	Mon, 02 Jun 2008 23:38:22 +0200
changeset 27048	0e86aab627f3
parent 27038	854c61598628
child 28751	aad88e7344f0
permissions	-rw-r--r--