doc-src/IsarAdvanced/Classes/style.sty
author wenzelm
Sat Oct 04 16:05:09 2008 +0200 (2008-10-04 ago)
changeset 28500 4b79e5d3d0aa
parent 26781 861e06a047c5
child 29016 31110b40eae7
permissions -rw-r--r--
replaced ISATOOL by ISABELLE_TOOL;
haftmann@20946
     1
haftmann@20946
     2
%% $Id$
haftmann@20946
     3
haftmann@20946
     4
%% toc
haftmann@20946
     5
\newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}
haftmann@20946
     6
\@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}}
haftmann@20946
     7
haftmann@20946
     8
%% references
haftmann@20946
     9
\newcommand{\secref}[1]{\S\ref{#1}}
haftmann@20946
    10
\newcommand{\chref}[1]{chapter~\ref{#1}}
haftmann@20946
    11
\newcommand{\figref}[1]{figure~\ref{#1}}
haftmann@20946
    12
haftmann@20946
    13
%% glossary
haftmann@20946
    14
\renewcommand{\glossary}[2]{\nomenclature{\bf #1}{#2}}
haftmann@20946
    15
\newcommand{\seeglossary}[1]{\emph{#1}}
haftmann@20946
    16
\newcommand{\glossaryname}{Glossary}
haftmann@20946
    17
\renewcommand{\nomname}{\glossaryname}
haftmann@20946
    18
\renewcommand{\pagedeclaration}[1]{\nobreak\quad\dotfill~page~\bold{#1}}
haftmann@20946
    19
haftmann@20946
    20
%% index
haftmann@20946
    21
\newcommand{\indexml}[1]{\index{\emph{#1}|bold}}
haftmann@20946
    22
\newcommand{\indexmltype}[1]{\index{\emph{#1} (type)|bold}}
haftmann@20946
    23
\newcommand{\indexmlstructure}[1]{\index{\emph{#1} (structure)|bold}}
haftmann@20946
    24
\newcommand{\indexmlfunctor}[1]{\index{\emph{#1} (functor)|bold}}
haftmann@20946
    25
haftmann@20946
    26
%% math
haftmann@20946
    27
\newcommand{\text}[1]{\mbox{#1}}
haftmann@20946
    28
\newcommand{\isasymvartheta}{\isamath{\theta}}
haftmann@20946
    29
\newcommand{\isactrlvec}[1]{\emph{$\overline{#1}$}}
haftmann@20946
    30
haftmann@20946
    31
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
haftmann@20946
    32
haftmann@20946
    33
\pagestyle{headings}
haftmann@20946
    34
\sloppy
haftmann@20946
    35
\binperiod
haftmann@20946
    36
\underscoreon
haftmann@20946
    37
haftmann@20946
    38
\renewcommand{\isadigit}[1]{\isamath{#1}}
haftmann@20946
    39
haftmann@20946
    40
\newenvironment{mldecls}{\par\noindent\begingroup\footnotesize\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\smallskip\endgroup}
haftmann@20946
    41
haftmann@20946
    42
\isafoldtag{FIXME}
haftmann@20946
    43
\isakeeptag{mlref}
haftmann@20946
    44
\renewcommand{\isatagmlref}{\subsection*{\makebox[0pt][r]{\fbox{\ML}~~}Reference}\begingroup\def\isastyletext{\rm}\small}
haftmann@20946
    45
\renewcommand{\endisatagmlref}{\endgroup}
haftmann@20946
    46
haftmann@20946
    47
\newcommand{\isasymGUESS}{\isakeyword{guess}}
haftmann@20946
    48
\newcommand{\isasymOBTAIN}{\isakeyword{obtain}}
haftmann@20946
    49
\newcommand{\isasymTHEORY}{\isakeyword{theory}}
haftmann@20946
    50
\newcommand{\isasymUSES}{\isakeyword{uses}}
haftmann@20946
    51
\newcommand{\isasymEND}{\isakeyword{end}}
haftmann@20946
    52
\newcommand{\isasymCONSTS}{\isakeyword{consts}}
haftmann@20946
    53
\newcommand{\isasymDEFS}{\isakeyword{defs}}
haftmann@20946
    54
\newcommand{\isasymTHEOREM}{\isakeyword{theorem}}
haftmann@20946
    55
\newcommand{\isasymDEFINITION}{\isakeyword{definition}}
haftmann@20946
    56
haftmann@20946
    57
\isabellestyle{it}
haftmann@20946
    58
haftmann@20946
    59
%%% Local Variables: 
haftmann@20946
    60
%%% mode: latex
haftmann@20946
    61
%%% TeX-master: "implementation"
haftmann@20946
    62
%%% End: