clear id
Prev Chapter 6. Tactics Next

clear id

clear H

Pre-conditions:

H must be an hypothesis of the current sequent to prove.

Action:

It hides the hypothesis H from the current sequent.

New sequents to prove:

None

Prev Up Next
auto [depth=nat] [width=nat] [paramodulation] [full] Home clearbody id