Skip to content
Snippets Groups Projects
Commit bd97b351 authored by Hans-Jörg's avatar Hans-Jörg
Browse files

Fix typo

parent 2493aeff
No related branches found
No related tags found
No related merge requests found
Pipeline #8255 passed
......@@ -21,7 +21,7 @@ $\grT{(assume }\dots\grT{)}$ command.
\proofsep& i.& \varphi &(\currule\; p_1, \dots, p_n)\; [a_1, \dots, a_n]\\
\end{plList}
\end{plContainer}
where $\varphi$ is any well formula.
where $\varphi$ is any well-formed formula.
This rule can be used to express holes in the proof. It can be used by
solvers as a placeholder for proof steps that are not yet expressed
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment