Skip to content
Snippets Groups Projects
Commit b07d98f6 authored by Daniel Plagge's avatar Daniel Plagge
Browse files

fix: "the rule is applicable ..." -> "the rule is not applicable"

git-svn-id: svn://svn.code.sf.net/p/rodin-b-sharp/svn/trunk/Handbook@15967 1434b563-b632-4741-aa49-43a3a8374d2e
parent 2bc13f57
No related branches found
No related tags found
No related merge requests found
...@@ -83,7 +83,7 @@ Where: ...@@ -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. 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} \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. \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} \end{itemize}
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment