- SYNOPSIS
-
Conversion that always succeeds and leaves a term unchanged.
- DESCRIPTION
-
When applied to a term `t`, the conversion ALL_CONV returns the
theorem |- t = t. It is just REFL explicitly regarded as a conversion.
- FAILURE CONDITIONS
-
Never fails.
- USES
-
Identity element for THENC.
- SEE ALSO
-
NO_CONV, REFL.