doc-src/Classes/classes.tex

generate proper arity declarations for TFrees for SPASS's DFG format;
and renamed a confusing function in the process

+
−
+
−\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 Isar type classes, which 
+
−  are a convenient mechanism for organizing specifications.
+
−  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: