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