A tactic language framework to ease proving theorems in HOL4.