Rodin User’s Handbook v.2.8: What do the labels on the proof tree mean?

Rodin Handbook

This work is sponsored by the Deploy Project

This work is sponsored by the ADVANCE Project

Creative Commons License

Creative Commons License

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

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

Rodin User’s Handbook v.2.8 : Frequently Asked Questions : Proving : What do the labels on the proof tree mean?