doc-src/IsarImplementation/style.sty
changeset 30240 5b25fee0362c
parent 26770 d688166808c0
child 30242 aea5d7fa7ef5
equal deleted inserted replaced
30239:179ff9cb160b 30240:5b25fee0362c
     1 
       
     2 %% $Id$
       
     3 
       
     4 %% toc
     1 %% toc
     5 \newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}
     2 \newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}
     6 \@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}}
     3 \@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}}
     7 
     4 
     8 %% references
     5 %% references
     9 \newcommand{\secref}[1]{\S\ref{#1}}
     6 \newcommand{\secref}[1]{\S\ref{#1}}
    10 \newcommand{\chref}[1]{chapter~\ref{#1}}
     7 \newcommand{\chref}[1]{chapter~\ref{#1}}
    11 \newcommand{\figref}[1]{figure~\ref{#1}}
     8 \newcommand{\figref}[1]{figure~\ref{#1}}
    12 
     9 
    13 %% glossary
       
    14 \renewcommand{\glossary}[2]{\nomenclature{\bf #1}{#2}}
       
    15 \newcommand{\seeglossary}[1]{\emph{#1}}
       
    16 \newcommand{\glossaryname}{Glossary}
       
    17 \renewcommand{\nomname}{\glossaryname}
       
    18 \renewcommand{\pagedeclaration}[1]{\nobreak\quad\dotfill~page~\bold{#1}}
       
    19 
       
    20 %% index
       
    21 \newcommand{\indexml}[1]{\index{\emph{#1}|bold}}
       
    22 \newcommand{\indexmlexception}[1]{\index{\emph{#1} (exception)|bold}}
       
    23 \newcommand{\indexmltype}[1]{\index{\emph{#1} (type)|bold}}
       
    24 \newcommand{\indexmlstructure}[1]{\index{\emph{#1} (structure)|bold}}
       
    25 \newcommand{\indexmlfunctor}[1]{\index{\emph{#1} (functor)|bold}}
       
    26 
       
    27 %% math
    10 %% math
    28 \newcommand{\text}[1]{\mbox{#1}}
    11 \newcommand{\text}[1]{\mbox{#1}}
    29 \newcommand{\isasymvartheta}{\isamath{\theta}}
    12 \newcommand{\isasymvartheta}{\isamath{\theta}}
    30 \newcommand{\isactrlvec}[1]{\emph{$\overline{#1}$}}
    13 \newcommand{\isactrlvec}[1]{\emph{$\vec{#1}$}}
       
    14 \newcommand{\isactrlBG}{\isacharbackquoteopen}
       
    15 \newcommand{\isactrlEN}{\isacharbackquoteclose}
    31 
    16 
    32 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
    17 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
    33 
    18 
    34 \pagestyle{headings}
    19 \pagestyle{headings}
    35 \sloppy
    20 \sloppy
    47 
    32 
    48 \newcommand{\minorcmd}[1]{{\sf #1}}
    33 \newcommand{\minorcmd}[1]{{\sf #1}}
    49 \newcommand{\isasymtype}{\minorcmd{type}}
    34 \newcommand{\isasymtype}{\minorcmd{type}}
    50 \newcommand{\isasymval}{\minorcmd{val}}
    35 \newcommand{\isasymval}{\minorcmd{val}}
    51 
    36 
       
    37 \newcommand{\isasymFIX}{\isakeyword{fix}}
       
    38 \newcommand{\isasymASSUME}{\isakeyword{assume}}
       
    39 \newcommand{\isasymDEFINE}{\isakeyword{define}}
       
    40 \newcommand{\isasymNOTE}{\isakeyword{note}}
    52 \newcommand{\isasymGUESS}{\isakeyword{guess}}
    41 \newcommand{\isasymGUESS}{\isakeyword{guess}}
    53 \newcommand{\isasymOBTAIN}{\isakeyword{obtain}}
    42 \newcommand{\isasymOBTAIN}{\isakeyword{obtain}}
    54 \newcommand{\isasymTHEORY}{\isakeyword{theory}}
    43 \newcommand{\isasymTHEORY}{\isakeyword{theory}}
    55 \newcommand{\isasymUSES}{\isakeyword{uses}}
    44 \newcommand{\isasymUSES}{\isakeyword{uses}}
    56 \newcommand{\isasymEND}{\isakeyword{end}}
    45 \newcommand{\isasymEND}{\isakeyword{end}}
    59 \newcommand{\isasymTHEOREM}{\isakeyword{theorem}}
    48 \newcommand{\isasymTHEOREM}{\isakeyword{theorem}}
    60 \newcommand{\isasymDEFINITION}{\isakeyword{definition}}
    49 \newcommand{\isasymDEFINITION}{\isakeyword{definition}}
    61 
    50 
    62 \isabellestyle{it}
    51 \isabellestyle{it}
    63 
    52 
       
    53 
    64 %%% Local Variables: 
    54 %%% Local Variables: 
    65 %%% mode: latex
    55 %%% mode: latex
    66 %%% TeX-master: "implementation"
    56 %%% TeX-master: "implementation"
    67 %%% End: 
    57 %%% End: