From b07d98f6602f155793881d274c9ca1752808b524 Mon Sep 17 00:00:00 2001
From: Daniel Plagge <plagge@cs.uni-duesseldorf.de>
Date: Thu, 10 Oct 2013 10:13:36 +0000
Subject: [PATCH] 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
---
org.rodinp.handbook.feature/latex/reference-04.tex | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/org.rodinp.handbook.feature/latex/reference-04.tex b/org.rodinp.handbook.feature/latex/reference-04.tex
index ab4ad10..5bd1a02 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}
--
GitLab