HOL-ex.While_Combinator_Example