doc-src/IsarRef/isar-ref.tex
changeset 7050 c70d3402fef5
parent 7046 9f755ff43cff
child 7134 320b412e5800
equal deleted inserted replaced
7049:f59d33c6e1c7 7050:c70d3402fef5
     1 
     1 
     2 %% $Id$
     2 %% $Id$
     3 
     3 
     4 \documentclass[12pt]{report}
     4 \documentclass[12pt]{report}
     5 \usepackage{graphicx,a4,../iman,../extra,../proof,../rail,../pdfsetup}
     5 \usepackage{graphicx,a4,../iman,../extra,../proof,../rail,../isar,../pdfsetup}
     6 
     6 
     7 \title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] The Isabelle/Isar Reference Manual}
     7 \title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] The Isabelle/Isar Reference Manual}
       
     8 \author{\emph{Markus Wenzel} \\ TU M\"unchen}
     8 
     9 
     9 \author{\emph{Markus Wenzel} \\ TU M\"unchen}
    10 \makeindex
       
    11 
    10 
    12 
    11 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
    13 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
    12 
    14 
    13 \pagestyle{headings}
    15 \pagestyle{headings}
    14 \sloppy
    16 \sloppy
    17 \railalias{lbrace}{\ttlbrace}
    19 \railalias{lbrace}{\ttlbrace}
    18 \railalias{rbrace}{\ttrbrace}
    20 \railalias{rbrace}{\ttrbrace}
    19 \railterm{lbrace,rbrace}
    21 \railterm{lbrace,rbrace}
    20 
    22 
    21 \railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim}
    23 \railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim}
       
    24 \railterm{name,nameref,text,type,term,prop,atom}
    22 
    25 
       
    26 \makeatletter
       
    27 \newcommand{\railtoken}[1]{{\rail@termfont{#1}}}
       
    28 \newcommand{\railnonterm}[1]{{\rail@nontfont{#1}}}
       
    29 \makeatother
       
    30 
       
    31 \newcommand\indexoutertoken[1]{\index{#1@\railtoken{#1} (outer syntax)|bold}}
       
    32 \newcommand\indexouternonterm[1]{\index{#1@\railnonterm{#1} (outer syntax)|bold}}
    23 
    33 
    24 \begin{document}
    34 \begin{document}
    25 
    35 
    26 \underscoreoff
    36 \underscoreoff
    27 
    37