Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
doc-src/AxClass/Group/document/Product.tex
changeset 26871 996add9defab
parent 17187 45bee2f6e61f 
--- a/doc-src/AxClass/Group/document/Product.tex	Sat May 10 00:14:00 2008 +0200
+++ b/doc-src/AxClass/Group/document/Product.tex	Sat May 10 13:26:25 2008 +0200
@@ -52,10 +52,11 @@
   purely logical meaning is concerned \cite{Wenzel:1997:TPHOL}.
 
   On the other hand there are syntactic differences, of course.
-  Constants \isa{{\isasymodot}} on some type \isa{{\isasymtau}} are rejected by the
-  type-checker, unless the arity \isa{{\isasymtau}\ {\isasymColon}\ product} is part of the
-  type signature.  In our example, this arity may be always added when
-  required by means of an $\INSTANCE$ with the default proof $\DDOT$.
+ Constants \isa{{\isasymodot}} on some type \isa{{\isasymtau}} are rejected by the
+ type-checker, unless the arity \isa{{\isasymtau}\ {\isasymColon}\ product} is part of the
+ type signature.  In our example, this arity may be always added when
+ required by means of an \isakeyword{instance} with the default proof
+ (double-dot).
 
   \medskip Thus, we may observe the following discipline of using
   syntactic classes.  Overloaded polymorphic constants have their type
@@ -91,12 +92,12 @@
  well-formed only after the arity \isa{bool\ {\isasymColon}\ product} is made
  known to the type checker.
 
- \medskip It is very important to see that above $\DEFS$ are not
- directly connected with $\INSTANCE$ at all!  We were just following
- our convention to specify \isa{{\isasymodot}} on \isa{bool} after having
- instantiated \isa{bool\ {\isasymColon}\ product}.  Isabelle does not require
- these definitions, which is in contrast to programming languages like
- Haskell \cite{haskell-report}.
+ \medskip It is very important to see that above \isakeyword{defs} are
+ not directly connected with \isakeyword{instance} at all!  We were
+ just following our convention to specify \isa{{\isasymodot}} on \isa{bool}
+ after having instantiated \isa{bool\ {\isasymColon}\ product}.  Isabelle does
+ not require these definitions, which is in contrast to programming
+ languages like Haskell \cite{haskell-report}.
 
  \medskip While Isabelle type classes and those of Haskell are almost
  the same as far as type-checking and type inference are concerned,
isabelle