doc-src/Codegen/style.sty

generalize and shorten proof of basis_orthogonal

%% toc
\newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}
\@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}}

%% paragraphs
\setlength{\parindent}{1em}

%% references
\newcommand{\secref}[1]{\S\ref{#1}}
\newcommand{\figref}[1]{figure~\ref{#1}}

%% logical markup
\newcommand{\strong}[1]{{\bfseries {#1}}}
\newcommand{\qn}[1]{\emph{#1}}

%% typographic conventions
\newcommand{\qt}[1]{``{#1}''}
\newcommand{\ditem}[1]{\item[\isastyletext #1]}

%% quote environment
\isakeeptag{quote}
\renewenvironment{quote}
  {\list{}{\leftmargin2em\rightmargin0pt}\parindent0pt\parskip0pt\item\relax}
  {\endlist}
\renewcommand{\isatagquote}{\begin{quote}}
\renewcommand{\endisatagquote}{\end{quote}}
\newcommand{\quotebreak}{\\[1.2ex]}

%% typewriter text
\newenvironment{typewriter}{\renewcommand{\isastyletext}{}%
\renewcommand{\isadigit}[1]{{##1}}%
\parindent0pt%
\makeatletter\isa@parindent0pt\makeatother%
\isabellestyle{tt}\isastyle%
\fontsize{9pt}{9pt}\selectfont}{}

\isakeeptag{quotetypewriter}
\renewcommand{\isatagquotetypewriter}{\begin{quote}\begin{typewriter}}
\renewcommand{\endisatagquotetypewriter}{\end{typewriter}\end{quote}}

\isakeeptag{quotett}
\renewcommand{\isatagquotett}{\begin{quote}\isabellestyle{tt}\isastyle}
\renewcommand{\endisatagquotett}{\end{quote}}

%% a trick
\newcommand{\isasymSML}{SML}
\newcommand{\isasymSMLdummy}{SML}

%% presentation
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}

%% character detail
\renewcommand{\isadigit}[1]{\isamath{#1}}
\binperiod
\underscoreoff

%% format
\pagestyle{headings}
\isabellestyle{it}

%% ml reference
\newenvironment{mldecls}{\par\noindent\begingroup\footnotesize\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\smallskip\endgroup}

\isakeeptag{mlref}
\renewcommand{\isatagmlref}{\subsection*{\makebox[0pt][r]{\fbox{\ML}~~}Reference}\begingroup\def\isastyletext{\rm}\small}
\renewcommand{\endisatagmlref}{\endgroup}

\isabellestyle{it}


%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "implementation"
%%% End: