1signature ANF =
2sig
3  include Abbrev
4
5  type env = (term * (bool * thm * thm * thm)) list
6
7  val toComb : thm -> bool * term * term * thm
8  val toANF : env -> thm -> env
9
10  val std_bvars : string -> term -> term
11  val STD_BVARS : string -> thm -> thm
12  val STD_BVARS_CONV : string -> conv
13  val STD_BVARS_TAC : string -> tactic
14end
15