%% ODER: format ==         = "\mathrel{==}"
%% ODER: format /=         = "\neq "
%
%
\makeatletter
\@ifundefined{lhs2tex.lhs2tex.sty.read}%
  {\@namedef{lhs2tex.lhs2tex.sty.read}{}%
   \newcommand\SkipToFmtEnd{}%
   \newcommand\EndFmtInput{}%
   \long\def\SkipToFmtEnd#1\EndFmtInput{}%
  }\SkipToFmtEnd

\newcommand\ReadOnlyOnce[1]{\@ifundefined{#1}{\@namedef{#1}{}}\SkipToFmtEnd}
\usepackage{amstext}
\usepackage{amssymb}
\usepackage{stmaryrd}
\DeclareFontFamily{OT1}{cmtex}{}
\DeclareFontShape{OT1}{cmtex}{m}{n}
  {<5><6><7><8>cmtex8
   <9>cmtex9
   <10><10.95><12><14.4><17.28><20.74><24.88>cmtex10}{}
\DeclareFontShape{OT1}{cmtex}{m}{it}
  {<-> ssub * cmtt/m/it}{}
\newcommand{\texfamily}{\fontfamily{cmtex}\selectfont}
\DeclareFontShape{OT1}{cmtt}{bx}{n}
  {<5><6><7><8>cmtt8
   <9>cmbtt9
   <10><10.95><12><14.4><17.28><20.74><24.88>cmbtt10}{}
\DeclareFontShape{OT1}{cmtex}{bx}{n}
  {<-> ssub * cmtt/bx/n}{}
\newcommand{\tex}[1]{\text{\texfamily#1}}	% NEU

\newcommand{\Sp}{\hskip.33334em\relax}


\newcommand{\Conid}[1]{\mathit{#1}}
\newcommand{\Varid}[1]{\mathit{#1}}
\newcommand{\anonymous}{\kern0.06em \vbox{\hrule\@width.5em}}
\newcommand{\plus}{\mathbin{+\!\!\!+}}
\newcommand{\bind}{\mathbin{>\!\!\!>\mkern-6.7mu=}}
\newcommand{\sequ}{\mathbin{>\!\!\!>}}
\renewcommand{\leq}{\leqslant}
\renewcommand{\geq}{\geqslant}
\usepackage{polytable}

%mathindent has to be defined
\@ifundefined{mathindent}%
  {\newdimen\mathindent\mathindent\leftmargini}%
  {}%

\def\resethooks{%
  \global\let\SaveRestoreHook\empty
  \global\let\ColumnHook\empty}
\newcommand*{\savecolumns}[1][default]%
  {\g@addto@macro\SaveRestoreHook{\savecolumns[#1]}}
\newcommand*{\restorecolumns}[1][default]%
  {\g@addto@macro\SaveRestoreHook{\restorecolumns[#1]}}
\newcommand*{\aligncolumn}[2]%
  {\g@addto@macro\ColumnHook{\column{#1}{#2}}}

\resethooks

\newcommand{\onelinecommentchars}{\quad-{}- }
\newcommand{\commentbeginchars}{\enskip\{-}
\newcommand{\commentendchars}{-\}\enskip}

\newcommand{\visiblecomments}{%
  \let\onelinecomment=\onelinecommentchars
  \let\commentbegin=\commentbeginchars
  \let\commentend=\commentendchars}

\newcommand{\invisiblecomments}{%
  \let\onelinecomment=\empty
  \let\commentbegin=\empty
  \let\commentend=\empty}

\visiblecomments

\newlength{\blanklineskip}
\setlength{\blanklineskip}{1mm}

\newcommand{\hsindent}[1]{\quad}% default is fixed indentation
\newcommand{\NB}{\textbf{NB}}
\newcommand{\Todo}[1]{$\langle$\textbf{To do:}~#1$\rangle$}

\makeatother
\EndFmtInput
%
%% configuration




%% end of configuration

%% CONFIG: Omitted material excluded




% format * = "\times "
% subst inline a  	= "\ensuremath{{}\allowforspacecorrection " a "}"
% subst varid a  	= a "{}\allowforspacecorrection "








%% handling of `


















% format CnstrVarpi	= Cnstr "^{" varpi "}"


















% format <=> 			= "\mathrel{\cong}"
% format <+-> 			= "\setbox0=\hbox{\ensuremath{\mathrel{\vartriangle}}}\copy0\kern-.4\wd0\mathrel{\triangledown}"
% format +	 			= ","
% format ++	 			= ","



% format fiopt			= "{\xi}"





% format ANY				= "\makebox[0cm][l]{\(\top\)}\bot{}"




% format ftv				= "\ftv "










%% acronyms



% list environments
\def\@ListSetupA{%
}
\def\@ListSetupB{%
}

\newenvironment{Itemize}{%
  \@ListSetupA
  \begin{itemize}
  \@ListSetupB
}{%
  \end{itemize}
}

\newenvironment{Enumerate}{%
  \@ListSetupA
  \begin{enumerate}
  \@ListSetupB
}{%
  \end{enumerate}
}

% xfig figure
\newcommand{\FigCenterXFigTex}[1]{%
 \begin{center}
 \input #1.tex
 \end{center}
}

\newcommand{\FigScaledEPS}[2]{%
 \includegraphics[scale=#1]{#2.eps}
}

\newcommand{\FigEPS}[1]{%
 \FigScaledEPS{1}{#1}
}

\newcommand{\FigScaledPDF}[2]{%
 \includegraphics[scale=#1]{#2.pdf}
}

\newcommand{\FigScaledJPEG}[2]{%
 \includegraphics[scale=#1]{#2.jpg}
}

\newcommand{\FigPDF}[1]{%
 \FigScaledPDF{1}{#1}
}

\newcommand{\FigCenteredScaledPDF}[2]{%
 \begin{center}
 \includegraphics[scale=#1]{#2.pdf}
 \end{center}
}

\newcommand{\FigCenterPDF}[2]{%
 \begin{center}
 \FigScaledPDF{#1}{#2}
 \end{center}
}

%% AFP TeX macro's
\def\spacecorrection{\;}
\def\isspacecorrection{\spacecorrection}
\def\allowforspacecorrection#1{%
  \gdef\temp{#1}%
  \ifx\isspacecorrection\temp
    \let\next=\empty
  \else
    \let\next=\temp
  \fi
  \next}

\newcommand{\chooseFigPos}[1]{%
 %\def\CFP@@Pos{#1}
 \def\CFP@Pos{}
 \def\CFP@Tail{{figure}[\CFP@Pos]}
 \ifx\CFP@Pos\empty
  \begin{figure}[htbp]%
 \else\expandafter\begin\CFP@Tail\fi
}

% Env for figure
\newenvironment{Figure}[3]{%
  \def\F@Pos{\chooseFigPos{#1}}
  \def\F@Cap{#2}
  \def\F@Lab{#3}
  \F@Pos
}{%
  \caption{\F@Cap}
  \label{\F@Lab}
  \end{figure}
}

\newenvironment{CenterFigure}[3]{%
  \def\F@Pos{\chooseFigPos{#1}}
  \def\F@Cap{#2}
  \def\F@Lab{#3}
  \F@Pos
  \begin{center}
}{%
  \end{center}
  \caption{\F@Cap}
  \label{\F@Lab}
  \end{figure}
}

% Env for tabular figure
\newenvironment{TabularFigure}[4]{%
  \begin{Figure}{#1}{#2}{#3}
  \begin{tabular}{#4}
  \hline
%  \\
}{%
  \\
  \hline
  \end{tabular}
  \end{Figure}
}

% Env for centered tabular figure
\newenvironment{TabularCenterFigure}[4]{%
  \begin{CenterFigure}{#1}{#2}{#3}
  \begin{tabular}{#4}
  \hline
%  \\
}{%
  \\
  \hline
  \end{tabular}
  \end{CenterFigure}
}

% Plain figure
\newenvironment{PlainFigure}[3]{%
  \begin{TabularFigure}{#1}{#2}{#3}{p{.98\linewidth}}
}{%
  \end{TabularFigure}
}

% Plain figure
\newenvironment{PlainCenterFigure}[3]{%
  \begin{PlainFigure}{#1}{#2}{#3}
  \begin{center}
}{%
  \end{center}
  \end{PlainFigure}
}

% Env for xfig in a figure
\newenvironment{XFigFigure}[4]{%
  \begin{PlainFigure}{#1}{#3}{#4}
  \FigCenterXFigTex{#2}
}{%
  \end{PlainFigure}
}

% Cmd for pdf (from xfig) in a figure
\newcommand{\FigurePDF}[5]{%
  \begin{PlainFigure}{#1}{#4}{#5}
  \FigCenterPDF{#2}{#3}
  \end{PlainFigure}
}

% Cmd for pdf (from xfig) in a figure
\newcommand{\FigureXFigTex}[4]{%
  \begin{PlainFigure}{#1}{#3}{#4}
  \FigCenterXFigTex{#2}
  \end{PlainFigure}
}

% Env for rules in a figure
\newenvironment{RulesFigure}[3]{%
  \begin{TabularFigure}{}{#2}{#3}{P}
  \fbox{#1}
  \\
}{%
  \end{TabularFigure}
}

% Env for rules in a figure
% #1: scheme (displayed as judgement)
% #2: caption text
% #3: ruleset name
% #4: view name
\newenvironment{rulerRulesetFigure}[4]{%
  \def\R@Version{#4}
  \def\R@Info{\ifx\R@Version\empty #2\else #2 (\R@Version)\fi}
  \begin{TabularCenterFigure}{}{\R@Info}{#3}{p{0.95\linewidth}}
  \begin{center}
  \fbox{#1}
  \\
}{%
  \par
  \csname RulesFigureBEndHook\endcsname
  \end{center}
  \end{TabularCenterFigure}
}

% Cmd for single rule, name horizontally
% #1: rule name
% #2: view name
% #3: premise judgements
% #4: conclusion judgement
\newcommand{\rulerRule}[4]{%
\begingroup
\renewcommand{\arraystretch}{1}%
\mbox{%
\ensuremath{%
  \frac{%
    \begin{array}{@{}c@{}}%
    \ \\
    #3
    \end{array}%
  }{%
    \begin{array}{@{}c@{}}%
    #4
    \end{array}%
  }%
  \, \textsc{#1}_{#2}%
 }%
}
\endgroup
}

% Cmd for single rule, name vertically
% #1: rule name
% #2: view name
% #3: premise judgements
% #4: conclusion judgement
\newcommand{\rulerRuleVert}[4]{%
\begingroup
\renewcommand{\arraystretch}{1}%
\begin{array}{@{}l@{}}
\mbox{%
\ensuremath{%
  \frac{%
    \begin{array}{@{}c@{}}%
    \ \\
    #3
    \end{array}%
  }{%
    \begin{array}{@{}c@{}}%
    #4
    \end{array}%
  }%
 }%
}
\\
(\textsc{#1}_{#2})%
\\
\end{array}
\endgroup
}

% Old style
\newcommand{\ehinfrule}[4]{%
\begingroup
%\linespread{1}\selectfont
\renewcommand{\arraystretch}{1}%
\mbox{%
%\linespread{1}\selectfont
%\vspace{.5\baselineskip}
\ensuremath{%
  \frac{%
    \begin{array}{@{}c@{}}%
    %\renewcommand{\arraystretch}{1}%
    #3
    \end{array}%
  }{%
    \begin{array}{@{}c@{}}%
    %\renewcommand{\arraystretch}{1}%
    #4
    \end{array}%
  }%
  \, \textsc{#1}_{#2}%
 }%
}
\endgroup
}

% Env for code in a figure
\newenvironment{CodeFigure}[3]{%
  \begin{TabularFigure}{#1}{#2}{#3}{c}
  \begin{minipage}{0.9\textwidth}
  %\vspace{.5ex}
}{%
  %\vspace{.5ex}
  \end{minipage}
  \end{TabularFigure}
}

% safe way of using code env in slides
%\newcommand{\BoxCode}[1]{\parbox{\textwidth}{#1}}
\newcommand{\BoxCode}[1]{\parbox{\textwidth}{#1}}

% input
% 'If' depending on file existence
\newread\TmpRead
% IfInputExists( filename, exec-then, exec-else )
\def\IfInputExists#1#2#3{%
\immediate\openin\TmpRead=#1
\ifeof\TmpRead\immediate\closein\TmpRead\def\TmpA{#3}%
\else\immediate\closein\TmpRead\def\TmpA{#2}%
\fi\TmpA}
% input
\newcommand{\Input}[1]{\IfInputExists{#1}{\input{#1}}{}}

% stripAfterDot
\def\@stripAfterDot#1.#2;{#1}

% section structure related
\newcommand{\Paragraph}[1]{\paragraph{#1}}

% chunk related
\newcommand{\chunkHideDef}[2]{%
 \subsection{#2}\label{#1}
}
\newcommand{\chunkHideRefAppx}[1]{\marginpar[{\hfill\footnotesize\secPageRefB{#1}}]{{\footnotesize\secPageRefB{#1}}}}
\newcommand{\chunkHideRef}[1]{\chunkHideRefAppx{#1}}
\newcommand{\chunkCmdDef}[1]{\expandafter\def\csname #1\endcsname}
\newcommand{\chunkCmdUseRaw}[1]{%
 \csname #1\endcsname
}
\newcommand{\chunkCmdUse}[1]{%
 \chunkCmdUseRaw{#1}
 \vspace{-1.1ex}
}
\newcommand{\chunkCmdFrameUse}[1]{%
}
\newcommand{\chunkCmdUsePrevLit}[1]{{\color{blue}\chunkCmdUse{#1}}}
\newcommand{\chunkCmdUsePrev}[1]{\par\chunkRefsExpanded{#1}}
\newcommand{\chunkCmdUseOnPrev}[2]{%
{\chunkCmdUseMark{#2}}
% {\par{[see page(s)~\chunkRefs{#1}]}\setlength{\parskip}{0cm}\chunkCmdUseMark{#2}}
% {\par{\color{blue}...page(s)~\chunkRefs{#1}}\setlength{\parskip}{0cm}\chunkCmdUseMark{#2}}
}
\newcommand{\chunkMark}[1]{%
}
\newcommand{\chunkCmdUseMark}[1]{\chunkMark{#1}\chunkCmdUse{#1}}
\newcommand{\chunkIndex}[1]{\index{#1}}
\newcommand{\chunkRefs}[1]{\@for\@chunkRef:=#1\do{,~\pageref{\@chunkRef}}}
\newcommand{\chunkRefsExpanded}[1]{\@for\@chunkRef:=#1\do{{\color{blue}\chunkCmdUse{\@chunkRef}}\setlength{\parskip}{0cm}}}

% font usage
\newcommand{\textRL}[1]{\textsc{#1}}

% ruler related

% Cmd to define a ruler cmd (for rules, figures, ...)
% #1: cmd name
% #2: body
\newcommand{\rulerCmdDef}[1]{\expandafter\def\csname #1\endcsname}

% Cmd to use a ruler cmd (for rules, figures, ...)
% #1: cmd name
\newcommand{\rulerCmdUse}[1]{\csname #1\endcsname}

\newcommand{\rulerCmdUseExplain}[3]{%
 \begingroup
 \def\RulesFigureBEndHook{%
  \vspace{1.5ex}
  \small
  \renewcommand{\arraystretch}{1.2}
  \begin{tabular}{l@{\ :\ }p{.75\linewidth}}
   \hline\hline \multicolumn{2}{p{.85\linewidth}}{#2} \\\hline #3
  \end{tabular}
 }
 \def\RulesFigureBCaptionHook{, with explanation}
 \rulerCmdUse{#1}
 \endgroup
}
\newcommand{\ruleRef}[1]{rule~\textRL{#1}}
\newcommand{\RuleRef}[1]{Rule~\textsc{#1}}
\newcommand{\rulerChngBegMark}{\color{blue}}
\newcommand{\rulerChngEndMark}{\color{black}}
\newcommand{\rulerSameBegMark}{\color{gray!75}}
\newcommand{\rulerSameEndMark}{\color{black}}


% referencing
\newcommand{\refHideWWW}[1]{\marginpar[\hfill\WWWlogo]{\WWWlogo}}
\def\myRef#1{\ref{#1}}
\newcommand{\figRef}[1]{Fig.~\myRef{#1}}
\newcommand{\FigRef}[1]{Fig.~\myRef{#1}}
\newcommand{\secRef}[1]{Section~\myRef{#1}}
\newcommand{\exRef}[1]{Example~\myRef{#1}}
\newcommand{\thRef}[1]{Theorem~\myRef{#1}}
\newcommand{\pageRef}[1]{page~\pageref{#1}}
\newcommand{\pageRefB}[1]{p~\pageref{#1}}
\newcommand{\figPageRef}[1]{\figRef{#1}, \pageRef{#1}}
\newcommand{\secPageRef}[1]{\secRef{#1}, \pageRef{#1}}
\newcommand{\exPageRef}[1]{\exRef{#1}, \pageRef{#1}}
\newcommand{\thPageRef}[1]{\thRef{#1}, \pageRef{#1}}
\newcommand{\thPageRefB}[1]{\thRef{#1} (\pageRef{#1})}
\newcommand{\secPageRefB}[1]{\pageRefB{#1}, \myRef{#1}}
\newcommand{\chapterRef}[1]{%
Chapter~\myRef{#1}%
}
\let\chaptRef=\chapterRef
\newcommand{\appRef}[1]{appendix~\myRef{#1}}

% citations
\newcommand{\refPDF}[1]{%
\IfInputExists{#1}{({\color{blue}\href{#1}{pdf}})}{}
}
% \newcommand{\Cite}[1]{\cite{#1}\ifx#2\empty\else(#2)\fi\refPDF{papers/#1.pdf}}

% verbatim
\DefineVerbatimEnvironment%
 {TT}{Verbatim}
 {xleftmargin=.05\textwidth,fontsize=\small}
\DefineVerbatimEnvironment%
 {TTtiny}{Verbatim}
 {fontsize=\tiny}
\DefineVerbatimEnvironment%
 {TTfootnotesize}{Verbatim}
 {fontsize=\footnotesize}

% AG feature appearing later in the text, after the primer
\newenvironment{AGFeature}[2]{%
\label{#1}
\begin{description}
\item[\ensuremath{\mathcal{AG}}: #2.]
}{%
\end{description}
}

\newenvironment{AGFeatureLater}[2]{%
\item
\textbf{#2} \emph{(Context and example at \pageRef{#1})}:
}{%
}

% theorem env: example
\newtheorem{ExampleEnv}{Example}[chapter]
\newtheorem{Theorem}[ExampleEnv]{Theorem}
\newtheorem{Definition}[ExampleEnv]{Definition}
\newenvironment{Example}[1]{%
\begin{ExampleEnv}\ \label{#1}
}{%
\end{ExampleEnv}
}

%% overlay (to be sorted out, these are just placeholders)
\newcommand{\overlayChunks}[1]{}

%% handling of `

\def\obacktick{\mathop{\ifnum0=`}\fi`\mathord{\ifnum0=`}\fi\let\backtick\cbacktick}
\def\cbacktick{\ifnum0=`{\fi}`\ifnum0=`{\fi}}
\let\backtick\obacktick

% Indexing
\newcommand{\Ix}[1]{\index{#1}}
\newcommand{\IxDef}[1]{\Ix{#1}}
\newcommand{\IxUse}[1]{\Ix{#1}}
\newcommand{\IxAndDef}[1]{\emph{#1}\IxDef{#1}}
\newcommand{\IxAndUse}[1]{#1\IxUse{#1}}
% older variants:
\newcommand{\IxAsIs}[1]{\IxAndUse{#1}}
\newcommand{\IxAsDef}[1]{\IxAndDef{#1}}

% To be done
\def\TBD#1{{\color{red}TBD: #1}}

% slides
% \def\frame#1{}

% binary operators
%\newcommand{\bvartriangle}{\mathrel{\vartriangle}}
%\newcommand{\btriangledown}{\mathrel{\triangledown}}

% cfg for versions
\def\ifInfTwoPass#1#2{%
#2
}

\newsavebox{\blindbox}
\newlength{\blindboxwd}
\newlength{\blindboxht}
\newlength{\blindboxdp}
\newcommand{\blindtext}[1]{%
 \begin{lrbox}{\blindbox}#1\end{lrbox}%
 \settowidth{\blindboxwd}{\usebox{\blindbox}}%
 \settoheight{\blindboxht}{\usebox{\blindbox}}%
 \settodepth{\blindboxdp}{\usebox{\blindbox}}%
 \rule[-\blindboxdp]{\blindboxwd}{\blindboxht}%
}

\newcommand{\blind}[1]{#1}
\newcommand{\blindcite}[1]{\blind{\cite{#1}}}