The conceal command causes the inspected part of a goal to be replaced by ... in the on-screen presentation. The hidden formula can be resurrected later using the reveal command.
The conceal command is applicable to predicates and to expressions.
| p |  | ... |
| e | | ... |
"conceal" p e
This example applies the conceal command to predicate p and expression e. Its use in tactics typically arises from recording scripts.