--- a/doc-src/TutorialI/CTL/document/CTL.tex Fri Feb 16 08:10:28 2001 +0100
+++ b/doc-src/TutorialI/CTL/document/CTL.tex Fri Feb 16 08:27:17 2001 +0100
@@ -206,7 +206,7 @@
What is worth noting here is that we have used \isa{fast} rather than
\isa{blast}. The reason is that \isa{blast} would fail because it cannot
cope with \isa{someI{\isadigit{2}}{\isacharunderscore}ex}: unifying its conclusion with the current
-subgoal is nontrivial because of the nested schematic variables. For
+subgoal is non-trivial because of the nested schematic variables. For
efficiency reasons \isa{blast} does not even attempt such unifications.
Although \isa{fast} can in principle cope with complicated unification
problems, in practice the number of unifiers arising is often prohibitive and