clear
Prev Chapter 7. Tactics Next

clear

-H

Synopsis:

-id

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
macro_input Home constructor