This work is sponsored by the
Deploy Project
This work is sponsored by the
ADVANCE Project
This work is licensed under a Creative Commons Attribution 3.0 Unported License
What do the labels on the proof tree mean?
Rodin User’s Handbook v.2.8
 



Rodin User’s Handbook v.2.8 



4.4.3 What do the labels on the proof tree mean?
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 (3.1.7.4), sl/ds means selection/deselection, PP means discharged by the predicate prover, ML means discharged by the mono lemma prover
