doc-src/IsarImplementation/Thy/Syntax.thy

   "let"} bindings.  These are expanded during the @{text "check"}
   phase, and contracted during the @{text "uncheck"} phase, without
   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 @{command class} command defines a context where
   @{text "check"} treats certain type instances of overloaded
   constants according to the ``dictionary construction'' of its
   logical foundation.  This involves ``type improvement''