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

     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   Florian Haftmann,

    23   Gerwin Klein,

    24   Alexander Krauss, \\

    25   Tobias Nipkow,

    26   David von Oheimb,

    27   Larry Paulson, \\

    28   and Sebastian Skalberg

    29 }

    31 \makeindex

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

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

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

    37 \railalias{ident}{\railtok{ident}}

    38 \railalias{longident}{\railtok{longident}}

    39 \railalias{symident}{\railtok{symident}}

    40 \railalias{var}{\railtok{var}}

    41 \railalias{textvar}{\railtok{textvar}}

    42 \railalias{typefree}{\railtok{typefree}}

    43 \railalias{typevar}{\railtok{typevar}}

    44 \railalias{nat}{\railtok{nat}}

    45 \railalias{string}{\railtok{string}}

    46 \railalias{verbatim}{\railtok{verbatim}}

    47 \railalias{keyword}{\railtok{keyword}}

    49 \railalias{name}{\railqtok{name}}

    50 \railalias{nameref}{\railqtok{nameref}}

    51 \railalias{text}{\railqtok{text}}

    52 \railalias{type}{\railqtok{type}}

    53 \railalias{term}{\railqtok{term}}

    54 \railalias{prop}{\railqtok{prop}}

    55 \railalias{atom}{\railqtok{atom}}

    57 \railalias{subseteq}{\isasymsubseteq}\railterm{subseteq}

    58 \railalias{equiv}{\isasymequiv}\railterm{equiv}

    59 \railalias{rightleftharpoons}{\isasymrightleftharpoons}\railterm{rightleftharpoons}

    60 \railalias{rightharpoonup}{\isasymrightharpoonup}\railterm{rightharpoonup}

    61 \railalias{leftharpoondown}{\isasymleftharpoondown}\railterm{leftharpoondown}

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

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

    66 \chardef\charbackquote=`\`

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

    70 \begin{document}

    72 \maketitle

    74 \pagenumbering{roman} \tableofcontents \clearfirst

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

    77 \input{basics.tex}

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

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

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

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

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

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

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

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

    87 \appendix

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

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

    91 \begingroup

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

    93   \bibliography{../manual}

    94 \endgroup

    96 \printindex

    98 \end{document}

author	wenzelm
	Mon, 02 Jun 2008 21:01:42 +0200
changeset 27035	d038a2ba87f6
parent 26906	6e8152678e06
child 27037	33d95687514e
permissions	-rw-r--r--