IFC : conv -> conv -> conv -> conv
STRUCTURE
SYNOPSIS
Apply a conversion and branch to next conversion.
DESCRIPTION
A call to IFC c1 c2 c3 t applies the conversion c1 to t. If this application succeeds (or raises UNCHANGED) then c2 is applied next. Otherwise, c3 is applied to t.
FAILURE
Fails when c1 succeeds and c2 fails, or when c1 fails and c3 fails.
EXAMPLE
   > IFC (RATOR_CONV BETA_CONV) BETA_CONV NO_CONV ``(\x y. x ==> y) T F``;
   val it = |- T ==> F : thm
The first RATOR_CONV BETA_CONV succeeds and chains successfully with the second BETA_CONV.

   > IFC ALL_CONV BETA_CONV (RATOR_CONV BETA_CONV) ``(\x y. x ==> y) T F``;
   Exception - BETA_CONV: not a beta redex
Although ALL_CONV succeeds, it does nothing, so BETA_CONV is not applicable.

   > IFC NO_CONV BETA_CONV (RATOR_CONV BETA_CONV) ``(\x y. x ==> y) T F``;
   val it = |- (\y. T ==> y) F : thm
The NO_CONV fails, so RATOR_CONV BETA_CONV applies.
SEEALSO
HOL  Kananaskis-14