src/Doc/Eisbach/document/style.sty
changeset 60288 d7f636331176
child 61962 9c8fc56032e3
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Doc/Eisbach/document/style.sty	Sun May 17 23:03:49 2015 +0200
     1.3 @@ -0,0 +1,68 @@
     1.4 +%% toc
     1.5 +\newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}
     1.6 +\@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}}
     1.7 +
     1.8 +%% references
     1.9 +\newcommand{\secref}[1]{\S\ref{#1}}
    1.10 +\newcommand{\chref}[1]{chapter~\ref{#1}}
    1.11 +\newcommand{\figref}[1]{figure~\ref{#1}}
    1.12 +
    1.13 +%% math
    1.14 +\newcommand{\text}[1]{\mbox{#1}}
    1.15 +\newcommand{\isasymvartheta}{\isamath{\theta}}
    1.16 +\newcommand{\isactrlvec}[1]{\emph{$\vec{#1}$}}
    1.17 +\newcommand{\isactrlBG}{\isacharbackquoteopen}
    1.18 +\newcommand{\isactrlEN}{\isacharbackquoteclose}
    1.19 +
    1.20 +\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
    1.21 +
    1.22 +\pagestyle{headings}
    1.23 +\sloppy
    1.24 +\binperiod
    1.25 +
    1.26 +\parindent 0pt\parskip 0.5ex
    1.27 +
    1.28 +\renewcommand{\isadigit}[1]{\isamath{#1}}
    1.29 +
    1.30 +\newenvironment{mldecls}{\par\noindent\begingroup\footnotesize\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\smallskip\endgroup}
    1.31 +
    1.32 +\isafoldtag{FIXME}
    1.33 +
    1.34 +\isakeeptag{mlref}
    1.35 +\renewcommand{\isatagmlref}{\subsection*{\makebox[0pt][r]{\fbox{ML}~~}Reference}}
    1.36 +\renewcommand{\endisatagmlref}{}
    1.37 +
    1.38 +\isakeeptag{mlantiq}
    1.39 +\renewcommand{\isatagmlantiq}{\subsection*{\makebox[0pt][r]{\fbox{ML}~~}Antiquotations}}
    1.40 +\renewcommand{\endisatagmlantiq}{}
    1.41 +
    1.42 +\isakeeptag{mlex}
    1.43 +\renewcommand{\isatagmlex}{\subsection*{\makebox[0pt][r]{\fbox{ML}~~}Examples}}
    1.44 +\renewcommand{\endisatagmlex}{}
    1.45 +
    1.46 +\renewcommand{\isatagML}{\begingroup\isabellestyle{default}\isastyle\def\isadigit##1{##1}}
    1.47 +\renewcommand{\endisatagML}{\endgroup}
    1.48 +
    1.49 +\newcommand{\minorcmd}[1]{{\sf #1}}
    1.50 +\newcommand{\isasymtype}{\minorcmd{type}}
    1.51 +\newcommand{\isasymval}{\minorcmd{val}}
    1.52 +
    1.53 +\newcommand{\isasymFIX}{\isakeyword{fix}}
    1.54 +\newcommand{\isasymASSUME}{\isakeyword{assume}}
    1.55 +\newcommand{\isasymDEFINE}{\isakeyword{define}}
    1.56 +\newcommand{\isasymNOTE}{\isakeyword{note}}
    1.57 +\newcommand{\isasymGUESS}{\isakeyword{guess}}
    1.58 +\newcommand{\isasymOBTAIN}{\isakeyword{obtain}}
    1.59 +\newcommand{\isasymTHEORY}{\isakeyword{theory}}
    1.60 +\newcommand{\isasymUSES}{\isakeyword{uses}}
    1.61 +\newcommand{\isasymEND}{\isakeyword{end}}
    1.62 +\newcommand{\isasymCONSTS}{\isakeyword{consts}}
    1.63 +\newcommand{\isasymDEFS}{\isakeyword{defs}}
    1.64 +\newcommand{\isasymTHEOREM}{\isakeyword{theorem}}
    1.65 +\newcommand{\isasymDEFINITION}{\isakeyword{definition}}
    1.66 +
    1.67 +\isabellestyle{literal}
    1.68 +
    1.69 +\railtermfont{\isabellestyle{tt}}
    1.70 +\railnontermfont{\isabellestyle{itunderscore}}
    1.71 +\railnamefont{\isabellestyle{itunderscore}}