ALL_CONV : conv
STRUCTURE
Conv
SYNOPSIS
Conversion that always succeeds, raising the
UNCHANGED
exception.
DESCRIPTION
When applied to a term
t
, the conversion
ALL_CONV
raises the special
UNCHANGED
exception.
FAILURE
Never fails.
USES
Identity element for
THENC
.
SEEALSO
NO_CONV
,
REFL
HOL
Kananaskis-10