--- a/doc-src/Classes/Thy/document/Classes.tex Tue Mar 03 11:00:51 2009 +0100
+++ b/doc-src/Classes/Thy/document/Classes.tex Tue Mar 03 13:20:53 2009 +0100
@@ -18,10 +18,6 @@
%
\endisadelimtheory
%
-\isamarkupchapter{Haskell-style classes with Isabelle/Isar%
-}
-\isamarkuptrue%
-%
\isamarkupsection{Introduction%
}
\isamarkuptrue%
@@ -37,10 +33,11 @@
types for \isa{{\isasymalpha}}, which is achieved by splitting introduction
of the \isa{eq} function from its overloaded definitions by means
of \isa{class} and \isa{instance} declarations:
+ \footnote{syntax here is a kind of isabellized Haskell}
\begin{quote}
- \noindent\isa{class\ eq\ where}\footnote{syntax here is a kind of isabellized Haskell} \\
+ \noindent\isa{class\ eq\ where} \\
\hspace*{2ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool}
\medskip\noindent\isa{instance\ nat\ {\isasymColon}\ eq\ where} \\
@@ -597,24 +594,21 @@
\noindent essentially introduces the locale%
\end{isamarkuptext}%
\isamarkuptrue%
-%
+\ %
\isadeliminvisible
-\ %
+%
\endisadeliminvisible
%
\isataginvisible
-\isacommand{setup}\isamarkupfalse%
-\ {\isacharverbatimopen}\ Sign{\isachardot}add{\isacharunderscore}path\ {\isachardoublequote}foo{\isachardoublequote}\ {\isacharverbatimclose}%
+%
\endisataginvisible
{\isafoldinvisible}%
%
\isadeliminvisible
%
\endisadeliminvisible
-\isanewline
%
\isadelimquote
-\isanewline
%
\endisadelimquote
%
@@ -654,31 +648,28 @@
of a primitive axclass%
\end{isamarkuptext}%
\isamarkuptrue%
-%
+\ %
\isadeliminvisible
-\ %
+%
\endisadeliminvisible
%
\isataginvisible
-\isacommand{setup}\isamarkupfalse%
-\ {\isacharverbatimopen}\ Sign{\isachardot}add{\isacharunderscore}path\ {\isachardoublequote}foo{\isachardoublequote}\ {\isacharverbatimclose}%
+%
\endisataginvisible
{\isafoldinvisible}%
%
\isadeliminvisible
%
\endisadeliminvisible
-\isanewline
%
\isadelimquote
-\isanewline
%
\endisadelimquote
%
\isatagquote
\isacommand{axclass}\isamarkupfalse%
\ idem\ {\isacharless}\ type\isanewline
-\ \ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}%
+\ \ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}\ %
\endisatagquote
{\isafoldquote}%
%
@@ -687,12 +678,11 @@
\endisadelimquote
%
\isadeliminvisible
-\ %
+%
\endisadeliminvisible
%
\isataginvisible
-\isacommand{setup}\isamarkupfalse%
-\ {\isacharverbatimopen}\ Sign{\isachardot}parent{\isacharunderscore}path\ {\isacharverbatimclose}%
+%
\endisataginvisible
{\isafoldinvisible}%
%
@@ -729,14 +719,13 @@
to class \isa{idem}.%
\end{isamarkuptext}%
\isamarkuptrue%
-%
+\ %
\isadeliminvisible
-\ %
+%
\endisadeliminvisible
%
\isataginvisible
-\isacommand{setup}\isamarkupfalse%
-\ {\isacharverbatimopen}\ Sign{\isachardot}parent{\isacharunderscore}path\ {\isacharverbatimclose}%
+%
\endisataginvisible
{\isafoldinvisible}%
%
@@ -978,7 +967,7 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent The logical proof is carried out on the locale level.
+The logical proof is carried out on the locale level.
Afterwards it is propagated
to the type system, making \isa{group} an instance of
\isa{monoid} by adding an additional edge
@@ -1010,11 +999,11 @@
\end{picture}
\caption{Subclass relationship of monoids and groups:
before and after establishing the relationship
- \isa{group\ {\isasymsubseteq}\ monoid}; transitive edges left out.}
+ \isa{group\ {\isasymsubseteq}\ monoid}; transitive edges are left out.}
\label{fig:subclass}
\end{center}
\end{figure}
-7
+
For illustration, a derived definition
in \isa{group} which uses \isa{pow{\isacharunderscore}nat}:%
\end{isamarkuptext}%