wenzelm@26738: wenzelm@26738: %% $Id$ wenzelm@26738: wenzelm@26738: %% toc wenzelm@26738: \newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1} wenzelm@26738: \@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}} wenzelm@26738: wenzelm@26738: %% references wenzelm@26738: \newcommand{\secref}[1]{\S\ref{#1}} wenzelm@26738: \newcommand{\chref}[1]{chapter~\ref{#1}} wenzelm@26738: \newcommand{\figref}[1]{figure~\ref{#1}} wenzelm@26738: wenzelm@26738: %% index wenzelm@26738: %FIXME wenzelm@26738: wenzelm@26738: %% math wenzelm@26738: \newcommand{\text}[1]{\mbox{#1}} wenzelm@26738: \newcommand{\isasymvartheta}{\isamath{\theta}} wenzelm@26738: \newcommand{\isactrlvec}[1]{\emph{$\overline{#1}$}} wenzelm@26738: wenzelm@26738: \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} wenzelm@26738: wenzelm@26738: \pagestyle{headings} wenzelm@26738: \sloppy wenzelm@26738: \binperiod wenzelm@26738: \underscoreon wenzelm@26738: wenzelm@26738: \renewcommand{\isadigit}[1]{\isamath{#1}} wenzelm@26738: wenzelm@26738: \newcommand{\minorcmd}[1]{{\sf #1}} wenzelm@26738: wenzelm@26738: \newcommand{\isasymGUESS}{\isakeyword{guess}} wenzelm@26738: \newcommand{\isasymOBTAIN}{\isakeyword{obtain}} wenzelm@26738: \newcommand{\isasymTHEORY}{\isakeyword{theory}} wenzelm@26738: \newcommand{\isasymIMPORTS}{\isakeyword{imports}} wenzelm@26738: \newcommand{\isasymUSES}{\isakeyword{uses}} wenzelm@26738: \newcommand{\isasymBEGIN}{\isakeyword{begin}} wenzelm@26738: \newcommand{\isasymEND}{\isakeyword{end}} wenzelm@26738: \newcommand{\isasymCONSTS}{\isakeyword{consts}} wenzelm@26738: \newcommand{\isasymDEFS}{\isakeyword{defs}} wenzelm@26738: \newcommand{\isasymTHEOREM}{\isakeyword{theorem}} wenzelm@26738: \newcommand{\isasymDEFINITION}{\isakeyword{definition}} wenzelm@26738: wenzelm@26738: \isabellestyle{it} wenzelm@26738: wenzelm@26738: %%% Local Variables: wenzelm@26738: %%% mode: latex wenzelm@26738: %%% TeX-master: "implementation" wenzelm@26738: %%% End: