Matita Home

`clearbody H`

- Synopsis:
**clearbody***id*- Pre-conditions:
**H**must be an hypothesis of the current sequent to prove.- Action:
It hides the definiens of a definition in the current sequent context. Thus the definition becomes an hypothesis.

- New sequents to prove:
None.