The `simplification tac` built-in tactic simplifies core Z notation,
performing the same inferences as the `simp` family of tactics
defined in section `simplification`.
It is applicable to any predicate, expression, schema text or goal.
If applied to its own result, nothing changes.

The `simp` family of tactics are very similar to the `puff` family
of tactics defined in section `corelaws`,
but are intended to faithfully reflect the behaviour of
the `simplification tac` built-in tactic.

One caveat to the above is that the rewriting aspect of commands
such as `absorption` is not done by `simplification tac`.

"apply tactic" p e "simplification tac"

This example applies the `simplification tac` built-in tactic
to predicate `p` and expression `e`.

IT 28-Dec-2005