michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/blast/unit): typo

Browse source
This commit is contained in:
Daniel Selsam 2015-11-28 14:29:44 -08:00 committed by Leonardo de Moura
parent 2bf9989bd9
commit c604333af2
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/blast/unit/unit_action.h
View file

@ -12,7 +12,7 @@ namespace blast {
<tt>A_1 -> ... -> A_n -> B_1 \/ (B2 \/ ... \/ B_m)...)</tt>
Whenever all but one of the literals is present as a hypothesis with
the appropriate polarity, we instantiate and resolve and necessary
the appropriate polarity, we instantiate and resolve as necessary
to conclude a new literal.
Remark: we assume that a pre-processing step will put lemmas