diff --git a/org.rodinp.handbook.feature/latex/reference-04.tex b/org.rodinp.handbook.feature/latex/reference-04.tex index ab4ad1090155e8acaf7d6b77fe153cd3ad8faae6..5bd1a02290ddc1a0378654af89eb18b1eaed061f 100644 --- a/org.rodinp.handbook.feature/latex/reference-04.tex +++ b/org.rodinp.handbook.feature/latex/reference-04.tex @@ -83,7 +83,7 @@ Where: Given a proof rule of the form mentioned above, the following describes how to apply this rule to an input sequent. If the process is successful, a list of output sequences is produced. \begin{itemize} - \item The rule is applicable if the goal of the sequent is not exactly the same as the used goal or if any of the used hypotheses are not contained in the set of hypotheses of the input sequent. + \item The rule is not applicable if the goal of the sequent is not exactly the same as the used goal or if any of the used hypotheses are not contained in the set of hypotheses of the input sequent. \item If the rule is applicable, the antecedent sequents are returned. The goal of each antecedent sequent is the new goal. The hypotheses of each antecedent sequent are the union of the old hypotheses and added hypotheses of the corresponding antecedent. \end{itemize}