Commit ad03921b authored by Allan Blanchard's avatar Allan Blanchard

Apply suggestion to src/plugins/wp/doc/manual/wp_plugin.tex

parent f09cd666
...@@ -450,7 +450,7 @@ The user select any integer expression $e$ in the proof and a base value $b$ (wh ...@@ -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 $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 $\Delta\models\,G$ is first generalized into $\Delta',P(e)\models\,Q(e)$. Then
we proceed by strong (integer) induction over $n$ for 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)}{% \[\TACTIC{\Delta\models\,G(n)}{%
\begin{array}[t]{lll} \begin{array}[t]{lll}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment