src/Doc/IsarImplementation/document/style.sty
changeset 56420 b266e7a86485
parent 56419 f47de9e82b0f
child 56431 4eb88149c7b2
--- a/src/Doc/IsarImplementation/document/style.sty	Sat Apr 05 17:52:29 2014 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,68 +0,0 @@
-%% toc
-\newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}
-\@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}}
-
-%% references
-\newcommand{\secref}[1]{\S\ref{#1}}
-\newcommand{\chref}[1]{chapter~\ref{#1}}
-\newcommand{\figref}[1]{figure~\ref{#1}}
-
-%% math
-\newcommand{\text}[1]{\mbox{#1}}
-\newcommand{\isasymvartheta}{\isamath{\theta}}
-\newcommand{\isactrlvec}[1]{\emph{$\vec{#1}$}}
-\newcommand{\isactrlBG}{\isacharbackquoteopen}
-\newcommand{\isactrlEN}{\isacharbackquoteclose}
-
-\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
-
-\pagestyle{headings}
-\sloppy
-\binperiod
-
-\parindent 0pt\parskip 0.5ex
-
-\renewcommand{\isadigit}[1]{\isamath{#1}}
-
-\newenvironment{mldecls}{\par\noindent\begingroup\footnotesize\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\smallskip\endgroup}
-
-\isafoldtag{FIXME}
-
-\isakeeptag{mlref}
-\renewcommand{\isatagmlref}{\subsection*{\makebox[0pt][r]{\fbox{ML}~~}Reference}}
-\renewcommand{\endisatagmlref}{}
-
-\isakeeptag{mlantiq}
-\renewcommand{\isatagmlantiq}{\subsection*{\makebox[0pt][r]{\fbox{ML}~~}Antiquotations}}
-\renewcommand{\endisatagmlantiq}{}
-
-\isakeeptag{mlex}
-\renewcommand{\isatagmlex}{\subsection*{\makebox[0pt][r]{\fbox{ML}~~}Examples}}
-\renewcommand{\endisatagmlex}{}
-
-\renewcommand{\isatagML}{\begingroup\isabellestyle{default}\isastyle\def\isadigit##1{##1}}
-\renewcommand{\endisatagML}{\endgroup}
-
-\newcommand{\minorcmd}[1]{{\sf #1}}
-\newcommand{\isasymtype}{\minorcmd{type}}
-\newcommand{\isasymval}{\minorcmd{val}}
-
-\newcommand{\isasymFIX}{\isakeyword{fix}}
-\newcommand{\isasymASSUME}{\isakeyword{assume}}
-\newcommand{\isasymDEFINE}{\isakeyword{define}}
-\newcommand{\isasymNOTE}{\isakeyword{note}}
-\newcommand{\isasymGUESS}{\isakeyword{guess}}
-\newcommand{\isasymOBTAIN}{\isakeyword{obtain}}
-\newcommand{\isasymTHEORY}{\isakeyword{theory}}
-\newcommand{\isasymUSES}{\isakeyword{uses}}
-\newcommand{\isasymEND}{\isakeyword{end}}
-\newcommand{\isasymCONSTS}{\isakeyword{consts}}
-\newcommand{\isasymDEFS}{\isakeyword{defs}}
-\newcommand{\isasymTHEOREM}{\isakeyword{theorem}}
-\newcommand{\isasymDEFINITION}{\isakeyword{definition}}
-
-\isabellestyle{literal}
-
-\railtermfont{\isabellestyle{tt}}
-\railnontermfont{\isabellestyle{itunderscore}}
-\railnamefont{\isabellestyle{itunderscore}}