Commit e0153316 authored by Allan Blanchard's avatar Allan Blanchard

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

parent 326de583
......@@ -306,7 +306,7 @@ $$\TACTIC{\Delta\models\,G}{%
\end{array}} $$
\paragraph{Definition} Unfold predicate and logic function definition\\
The user simply select a term $f(e_1,\ldots,e_n)$ or a predicate $P(e_1,\ldots,e_n)$ which is replaced by its definition, when available.
The user simply select a term $f(e_1,\ldots,e_n)$ or a predicate $P(e_1,\ldots,e_n)$ which is replaced with its definition, when available.
\paragraph{Filter} Erase Hypotheses \\
The tactic is always applicable. It removes hypotheses from the goal on a variable used basis. When variables are compounds (record and arrays) a finer heuristics is used to detect which parts of the variable is relevant. A transitive closure of dependencies is also used. However, it is always possible that too many hypotheses are removed.
......
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