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

     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{Thy/document/isabelle,Thy/document/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
	Sat, 10 May 2008 00:14:00 +0200
changeset 26870	94bedbb34b92
parent 26869	3bc332135aa7
child 26900	e37358673f87
permissions	-rw-r--r--