# HG changeset patch # User wenzelm # Date 1274778829 -7200 # Node ID 9b27c3dccb01f1b837aec8db4f79adac7a0a2f8f # Parent d37b5a9bec146b6efd19b9e494e7c6a6889a2f68 updated generated files; diff -r d37b5a9bec14 -r 9b27c3dccb01 doc-src/IsarRef/Thy/document/Spec.tex --- 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