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