revisiting type annotations for Haskell: necessary type annotations are not inferred on the provided theorems but using the arguments and right hand sides, as these might differ in the case of constants with abstract code types
% iman.sty : Isabelle Manual Page Layout
%
\typeout{Document Style iman. Released 17 February 1994}
\hyphenation{Isa-belle man-u-script man-u-scripts ap-pen-dix mut-u-al-ly}
\hyphenation{data-type data-types co-data-type co-data-types }
\let\ts=\thinspace
%usage: \iflabelundefined{LABEL}{if not defined}{if defined}
\newcommand{\iflabelundefined}[1]{\@ifundefined{r@#1}}
%%%INDEXING use sedindex to process the index
\newcommand\seealso[2]{\emph{see also} #1}
\usepackage{makeidx}
%index, putting page numbers of definitions in boldface
\def\bold#1{\textbf{#1}}
\newcommand\fnote[1]{#1n}
\newcommand\indexbold[1]{\index{#1|bold}}
%for indexing constants, symbols, theorems, ...
\newcommand\cdx[1]{{\tt#1}\index{#1@{\tt#1} constant}}
\newcommand\sdx[1]{{\tt#1}\index{#1@{\tt#1} symbol}}
\newcommand\tdx[1]{{\tt#1}\index{#1@{\tt#1} theorem}}
\newcommand\tdxbold[1]{{\tt#1}\index{#1@{\tt#1} theorem|bold}}
\newcommand\mltydx[1]{{\tt#1}\index{#1@{\tt#1} ML type}}
\newcommand\xdx[1]{{\tt#1}\index{#1@{\tt#1} exception}}
\newcommand\ndx[1]{{\tt#1}\index{#1@{\tt#1} nonterminal}}
\newcommand\ndxbold[1]{{\tt#1}\index{#1@{\tt#1} nonterminal|bold}}
\newcommand\cldx[1]{{\tt#1}\index{#1@{\tt#1} class}}
\newcommand\tydx[1]{\textit{#1}\index{#1@{\textit{#1}} type}}
\newcommand\thydx[1]{{\tt#1}\index{#1@{\tt#1} theory}}
\newcommand\tooldx[1]{{\tt#1}\index{#1@{\tt#1} tool}}
\newcommand\settdx[1]{{\tt#1}\index{#1@{\tt#1} setting}}
%set argument in \tt font; at the same time, index using * prefix
\newcommand\rmindex[1]{{#1}\index{#1}\@}
\newcommand\ttindex[1]{{\tt#1}\index{*#1}\@}
\newcommand\ttindexbold[1]{{\tt#1}\index{*#1|bold}\@}
%set argument in \bf font and index in ROMAN font (for definitions in text!)
\newcommand\bfindex[1]{{\bf#1}\index{#1|bold}\@}
%%% underscores as ordinary characters, not for subscripting
%% use @ or \sb for subscripting; use \at for @
%% only works in \tt font
%% must not make _ an active char; would make \ttindex fail!
\gdef\underscoreoff{\catcode`\@=8\catcode`\_=\other}
\gdef\underscoreon{\catcode`\_=8\makeatother}
\chardef\other=12
\chardef\at=`\@
% alternative underscore
\def\_{\leavevmode\kern.06em\vbox{\hrule height.2ex width.3em}\hskip0.1em}
%%% \dquotes permits usage of "..." for \hbox{...} -- also taken from under.sty
{\catcode`\"=\active
\gdef\dquotes{\catcode`\"=\active \let"=\@mathText}%
\gdef\@mathText#1"{\hbox{\mathTextFont #1\/}}}
\def\mathTextFont{\frenchspacing\tt}
\def\dquotesoff{\catcode`\"=\other}
%%%% meta-logical connectives
\let\Forall=\bigwedge
\let\Imp=\Longrightarrow
\let\To=\Rightarrow
\newcommand{\PROP}{\mathop{\mathrm{PROP}}}
\newcommand{\Var}[1]{{?\!#1}}
\newcommand{\All}[1]{\Forall#1.} %quantification
%%%% ``WARNING'' environment
\def\dbend{\vtop to 0pt{\vss\hbox{\Huge\bf!}\vss}}
\newenvironment{warn}{\medskip\medbreak\begingroup \clubpenalty=10000
\small %%WAS\baselineskip=0.9\baselineskip
\noindent \ifdim\parindent > 0pt\hangindent\parindent\else\hangindent1.5em\fi
\hangafter=-2
\hbox to0pt{\hskip-\hangindent\dbend\hfill}\ignorespaces}%
{\par\endgroup\medbreak}
%%%% Standard logical symbols
\let\turn=\vdash
\let\conj=\wedge
\let\disj=\vee
\let\imp=\rightarrow
\let\bimp=\leftrightarrow
\newcommand\all[1]{\forall#1.} %quantification
\newcommand\ex[1]{\exists#1.}
\newcommand{\pair}[1]{\langle#1\rangle}
\newcommand{\lparr}{\mathopen{(\!|}}
\newcommand{\rparr}{\mathclose{|\!)}}
\newcommand{\fs}{\mathpunct{,\,}}
\newcommand{\ty}{\mathrel{::}}
\newcommand{\asn}{\mathrel{:=}}
\newcommand{\more}{\ldots}
\newcommand{\record}[1]{\lparr #1 \rparr}
\newcommand{\dtt}{\mathord.}
\newcommand\lbrakk{\mathopen{[\![}}
\newcommand\rbrakk{\mathclose{]\!]}}
\newcommand\List[1]{\lbrakk#1\rbrakk} %was \obj
\newcommand\vpile[1]{\begin{array}{c}#1\end{array}}
\newenvironment{matharray}[1]{\[\begin{array}{#1}}{\end{array}\]}
\newcommand{\Text}[1]{\mbox{#1}}
\DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D}
\newcommand{\dsh}{\mathit{\dshsym}}
\let\int=\cap
\let\un=\cup
\let\inter=\bigcap
\let\union=\bigcup
\def\ML{{\sc ml}}
\def\OBJ{{\sc obj}}
\def\AST{{\sc ast}}
%macros to change the treatment of symbols
\def\relsemicolon{\mathcode`\;="303B} %treat ; like a relation
\def\binperiod{\mathcode`\.="213A} %treat . like a binary operator
\def\binvert{\mathcode`\|="226A} %treat | like a binary operator
%redefinition of \sloppy and \fussy to use \emergencystretch
\def\sloppy{\tolerance2000 \hfuzz.5pt \vfuzz.5pt \emergencystretch=15pt}
\def\fussy{\tolerance200 \hfuzz.1pt \vfuzz.1pt \emergencystretch=0pt}
%non-bf version of description
\def\descrlabel#1{\hspace\labelsep #1}
\def\descr{\list{}{\labelwidth\z@ \itemindent-\leftmargin\let\makelabel\descrlabel}}
\let\enddescr\endlist
% The mathcodes for the letters A, ..., Z, a, ..., z are changed to
% generate text italic rather than math italic by default. This makes
% multi-letter identifiers look better. The mathcode for character c
% is set to |"7000| (variable family) + |"400| (text italic) + |c|.
%
\DeclareSymbolFont{italics}{\encodingdefault}{\rmdefault}{m}{it}%
\def\@setmcodes#1#2#3{{\count0=#1 \count1=#3
\loop \global\mathcode\count0=\count1 \ifnum \count0<#2
\advance\count0 by1 \advance\count1 by1 \repeat}}
\@setmcodes{`A}{`Z}{"7\hexnumber@\symitalics41}
\@setmcodes{`a}{`z}{"7\hexnumber@\symitalics61}