REPEATC : conv -> conv

SYNOPSIS
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