--- a/doc-src/IsarRef/Thy/document/Spec.tex Tue May 25 10:57:02 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Tue May 25 11:13:49 2010 +0200
@@ -694,7 +694,7 @@
background theory will be augmented by the proven type arities.
On the theory level, \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}~\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlsub n{\isacharparenright}s{\isachardoublequote}} provides a convenient way to instantiate a type class with no
- need to specifify operations: one can continue with the
+ need to specify operations: one can continue with the
instantiation proof immediately.
\item \hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}}~\isa{c} in a class context for class