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

     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{supertabular}

    11 \usepackage{style}

    12 \usepackage{../pdfsetup}

    14 \hyphenation{Isabelle}

    15 \hyphenation{Isar}

    17 \isadroptag{theory}

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

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

    20   With Contributions by

    21   Clemens Ballarin,

    22   Stefan Berghofer, \\

    23   Lucas Dixon,

    24   Florian Haftmann,

    25   Gerwin Klein, \\

    26   Alexander Krauss,

    27   Tobias Nipkow,

    28   David von Oheimb, \\

    29   Larry Paulson,

    30   and Sebastian Skalberg

    31 }

    33 \makeindex

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

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

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

    39 \railalias{ident}{\railtok{ident}}

    40 \railalias{longident}{\railtok{longident}}

    41 \railalias{symident}{\railtok{symident}}

    42 \railalias{var}{\railtok{var}}

    43 \railalias{textvar}{\railtok{textvar}}

    44 \railalias{typefree}{\railtok{typefree}}

    45 \railalias{typevar}{\railtok{typevar}}

    46 \railalias{nat}{\railtok{nat}}

    47 \railalias{string}{\railtok{string}}

    48 \railalias{verbatim}{\railtok{verbatim}}

    49 \railalias{keyword}{\railtok{keyword}}

    51 \railalias{name}{\railqtok{name}}

    52 \railalias{nameref}{\railqtok{nameref}}

    53 \railalias{text}{\railqtok{text}}

    54 \railalias{type}{\railqtok{type}}

    55 \railalias{term}{\railqtok{term}}

    56 \railalias{prop}{\railqtok{prop}}

    57 \railalias{atom}{\railqtok{atom}}

    59 \railalias{subseteq}{\isasymsubseteq}\railterm{subseteq}

    60 \railalias{equiv}{\isasymequiv}\railterm{equiv}

    61 \railalias{rightleftharpoons}{\isasymrightleftharpoons}\railterm{rightleftharpoons}

    62 \railalias{rightharpoonup}{\isasymrightharpoonup}\railterm{rightharpoonup}

    63 \railalias{leftharpoondown}{\isasymleftharpoondown}\railterm{leftharpoondown}

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

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

    68 \chardef\charbackquote=`\`

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

    72 \begin{document}

    74 \maketitle

    76 \pagenumbering{roman} \tableofcontents \clearfirst

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

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

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

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

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

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

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

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

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

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

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

    90 \appendix

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

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

    94 \begingroup

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

    96   \bibliography{../manual}

    97 \endgroup

    99 \printindex

   101 \end{document}

author	wenzelm
	Thu, 13 Nov 2008 21:57:50 +0100
changeset 28773	39b4cedb8433
parent 28762	f5d79aeffd81
child 28838	d5db6dfcb34a
permissions	-rw-r--r--