Repeatedly apply a conversion (zero or more times) until it fails.
DESCRIPTION
If c is a conversion effects a transformation of a term t to a term t',
that is if c maps t to the theorem |- t = t`, then REPEATC c is the
conversion that repeats this transformation as often as possible. More
exactly, if c maps the term `ti` to |- ti=t(i+1) for i from 1 to n,
but fails when applied to the n+1th term `t(n+1)`, then REPEATC c `t1`
returns |- t1 = t(n+1). And if c `t` fails, them REPEATC c `t` returns
|- t = t.
FAILURE CONDITIONS
Never fails, but can diverge if the supplied conversion never fails.
EXAMPLE
# BETA_CONV `(\x. (\y. x + y) (x + 1)) 1`;;
val it : thm = |- (\x. (\y. x + y) (x + 1)) 1 = (\y. 1 + y) (1 + 1)
# REPEATC BETA_CONV `(\x. (\y. x + y) (x + 1)) 1`;;
val it : thm = |- (\x. (\y. x + y) (x + 1)) 1 = 1 + 1 + 1