Added "nitpick_const_simp" attribute to Nominal primrec.
\documentclass[12pt,a4paper,fleqn]{article}\usepackage{latexsym,graphicx}\usepackage[refpage]{nomencl}\usepackage{../iman,../extra,../isar,../proof}\usepackage{../isabelle,../isabellesym}\usepackage{style}\usepackage{../pdfsetup}\hyphenation{Isabelle}\hyphenation{Isar}\isadroptag{theory}\title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] Haskell-style type classes with Isabelle/Isar}\author{\emph{Florian Haftmann}}\begin{document}\maketitle\begin{abstract} \noindent This tutorial introduces the look-and-feel of Isar type classes to the end-user; Isar type classes are a convenient mechanism for organizing specifications, overcoming some drawbacks of raw axiomatic type classes. Essentially, they combine an operational aspect (in the manner of Haskell) with a logical aspect, both managed uniformly.\end{abstract}\thispagestyle{empty}\clearpage\pagenumbering{roman}\clearfirst\input{Thy/document/Classes.tex}\begingroup\bibliographystyle{plain} \small\raggedright\frenchspacing\bibliography{../manual}\endgroup\end{document}%%% Local Variables: %%% mode: latex%%% TeX-master: t%%% End: