# HG changeset patch
# User bulwahn
# Date 1319449231 -7200
# Node ID 48295059cef303ac7f49c053a2fdb72d43f3ddf1
# Parent  d32872ce58ce964ca7b93f4cd7fd875c589094ef
fixed typo

diff -r d32872ce58ce -r 48295059cef3 doc-src/IsarImplementation/Thy/Syntax.thy
--- a/doc-src/IsarImplementation/Thy/Syntax.thy	Mon Oct 24 10:45:54 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/Syntax.thy	Mon Oct 24 11:40:31 2011 +0200
@@ -134,7 +134,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 @{command class} command defines a context where
   @{text "check"} treats certain type instances of overloaded
diff -r d32872ce58ce -r 48295059cef3 doc-src/IsarImplementation/Thy/document/Syntax.tex
--- 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