--- a/doc-src/IsarImplementation/Thy/document/Syntax.tex Mon Oct 24 10:45:54 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Syntax.tex Mon Oct 24 11:40:31 2011 +0200
@@ -187,7 +187,7 @@
affecting the type-assignment of the given terms.
\medskip The precise meaning of type checking depends on the context
- --- additional check/unckeck plugins might be defined in user space!
+ --- additional check/uncheck plugins might be defined in user space!
For example, the \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} command defines a context where
\isa{check} treats certain type instances of overloaded