--- a/doc-src/TutorialI/Types/Axioms.thy Wed Jun 17 10:34:02 2009 +0200
+++ b/doc-src/TutorialI/Types/Axioms.thy Wed Jun 17 11:00:14 2009 +0200
@@ -13,8 +13,7 @@
subsubsection {* Semigroups *}
-text{* We specify \emph{semigroups} as subclass of @{class plus}
-where certain axioms need to hold: *}
+text{* We specify \emph{semigroups} as subclass of @{class plus}: *}
class semigroup = plus +
assumes assoc: "(x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
@@ -35,8 +34,8 @@
"'a"} restricts instantiations of @{typ "'a"} to types of class
@{class semigroup} and during the proof enables us to use the fact
@{fact assoc} whose type parameter is itself constrained to class
-@{class semigroup}. The main advantage is that theorems can be proved
-in the abstract and freely reused for each instance.
+@{class semigroup}. The main advantage of classes is that theorems
+can be proved in the abstract and freely reused for each instance.
On instantiation, we have to give a proof that the given operations
obey the class axioms: *}
@@ -107,7 +106,7 @@
end
-text {* \noindent Unless in the above examples, we here have both
+text {* \noindent In contrast to the examples above, we here have both
specification of class operations and a non-trivial instance proof.
This covers products as well:
--- a/doc-src/TutorialI/Types/Overloading.thy Wed Jun 17 10:34:02 2009 +0200
+++ b/doc-src/TutorialI/Types/Overloading.thy Wed Jun 17 11:00:14 2009 +0200
@@ -16,7 +16,7 @@
text {* \noindent This introduces a new class @{class [source] plus},
along with a constant @{const [source] plus} with nice infix syntax.
@{const [source] plus} is also named \emph{class operation}. The type
-of @{const [source] plus} carries a sort constraint @{typ [source] "'a
+of @{const [source] plus} carries a class constraint @{typ [source] "'a
:: plus"} on its type variable, meaning that only types of class
@{class [source] plus} can be instantiated for @{typ [source] "'a"}.
To breathe life into @{class [source] plus} we need to declare a type
--- a/doc-src/TutorialI/Types/document/Axioms.tex Wed Jun 17 10:34:02 2009 +0200
+++ b/doc-src/TutorialI/Types/document/Axioms.tex Wed Jun 17 11:00:14 2009 +0200
@@ -36,8 +36,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-We specify \emph{semigroups} as subclass of \isa{plus}
-where certain axioms need to hold:%
+We specify \emph{semigroups} as subclass of \isa{plus}:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{class}\isamarkupfalse%
@@ -75,8 +74,8 @@
\noindent The \isa{semigroup} constraint on type \isa{{\isacharprime}a} restricts instantiations of \isa{{\isacharprime}a} to types of class
\isa{semigroup} and during the proof enables us to use the fact
\hyperlink{fact.assoc}{\mbox{\isa{assoc}}} whose type parameter is itself constrained to class
-\isa{semigroup}. The main advantage is that theorems can be proved
-in the abstract and freely reused for each instance.
+\isa{semigroup}. The main advantage of classes is that theorems
+can be proved in the abstract and freely reused for each instance.
On instantiation, we have to give a proof that the given operations
obey the class axioms:%
@@ -220,7 +219,7 @@
\isacommand{end}\isamarkupfalse%
%
\begin{isamarkuptext}%
-\noindent Unless in the above examples, we here have both
+\noindent In contrast to the examples above, we here have both
specification of class operations and a non-trivial instance proof.
This covers products as well:%
--- a/doc-src/TutorialI/Types/document/Overloading.tex Wed Jun 17 10:34:02 2009 +0200
+++ b/doc-src/TutorialI/Types/document/Overloading.tex Wed Jun 17 11:00:14 2009 +0200
@@ -37,7 +37,7 @@
\noindent This introduces a new class \isa{plus},
along with a constant \isa{plus} with nice infix syntax.
\isa{plus} is also named \emph{class operation}. The type
-of \isa{plus} carries a sort constraint \isa{{\isachardoublequote}{\isacharprime}a\ {\isacharcolon}{\isacharcolon}\ plus{\isachardoublequote}} on its type variable, meaning that only types of class
+of \isa{plus} carries a class constraint \isa{{\isachardoublequote}{\isacharprime}a\ {\isacharcolon}{\isacharcolon}\ plus{\isachardoublequote}} on its type variable, meaning that only types of class
\isa{plus} can be instantiated for \isa{{\isachardoublequote}{\isacharprime}a{\isachardoublequote}}.
To breathe life into \isa{plus} we need to declare a type
to be an \bfindex{instance} of \isa{plus}:%
--- a/doc-src/TutorialI/Types/numerics.tex Wed Jun 17 10:34:02 2009 +0200
+++ b/doc-src/TutorialI/Types/numerics.tex Wed Jun 17 11:00:14 2009 +0200
@@ -1,4 +1,3 @@
-% $Id$
\section{Numbers}
\label{sec:numbers}
@@ -82,14 +81,14 @@
\end{warn}
\begin{warn}
-\index{recdef@\isacommand {recdef} (command)!and numeric literals}
+\index{function@\isacommand {function} (command)!and numeric literals}
Numeric literals are not constructors and therefore
must not be used in patterns. For example, this declaration is
rejected:
\begin{isabelle}
-\isacommand{recdef}\ h\ "\isacharbraceleft \isacharbraceright "\isanewline
+\isacommand{function}\ h\ \isakeyword{where}\isanewline
"h\ 3\ =\ 2"\isanewline
-"h\ i\ \ =\ i"
+\isacharbar "h\ i\ \ =\ i"
\end{isabelle}
You should use a conditional expression instead:
@@ -531,7 +530,7 @@
\subsubsection{Raising to a Power}
-Another type class, \tcdx{ringppower}, specifies rings that also have
+Another type class, \tcdx{ordered\_idom}, specifies rings that also have
exponentation to a natural number power, defined using the obvious primitive
recursion. Theory \thydx{Power} proves various theorems, such as the
following.