Rodin Handbook
This work is sponsored by the Deploy Project
This work is licensed under a Creative Commons Attribution 3.0 Unported License
 |
 |
 |
User Manual for Rodin v.2.3 |  |
 |
 |
4.4.3 Labels of proof tree nodes explained
ah means add hypothesis,
eh means rewrite with equality from hypothesis from left to right,
he means rewrite with equality from hypothesis from right to left,
rv tells us that this goal has been manually reviewed (see 3.1.5.4),
sl/ds means selection/deselection,
PP means discharged by the predicate prover,
ML means discharged by the mono lemma prover
|
|
|
|
|
|