From ad03921b2c876664b5c641324e9613b040746111 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 5 Nov 2020 10:46:08 +0100
Subject: [PATCH] Apply suggestion to src/plugins/wp/doc/manual/wp_plugin.tex
---
src/plugins/wp/doc/manual/wp_plugin.tex | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index b40e0727ccf..cc03c5dab63 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -450,7 +450,7 @@ The user select any integer expression $e$ in the proof and a base value $b$ (wh
$e = b$ and then the cases $e < b$ and $b < e$. Formally, the goal
$\Delta\models\,G$ is first generalized into $\Delta',P(e)\models\,Q(e)$. Then
we proceed by strong (integer) induction over $n$ for
-$G(n) \equiv P(n)\models\,Q(n)$:
+$G(n) \equiv P(n)\Longrightarrow\,Q(n)$:
\[\TACTIC{\Delta\models\,G(n)}{%
\begin{array}[t]{lll}
--
GitLab