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

     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/intro.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
	Thu, 15 May 2008 18:12:24 +0200
changeset 26906	6e8152678e06
parent 26904	e90832d7196a
child 27035	d038a2ba87f6
permissions	-rw-r--r--