Lines Matching refs:list
21 type vars = term list * hol_type list
39 type fol_problem = {thms : thm1 list, hyps : thm1 list, query : formula1 list}
40 val recent_fol_problems : fol_problem list option ref
49 val build_map : parameters * string list * thm list -> logic_map
53 type Query = vars * term list
54 type Result = vars * thm list
61 val FOL_NORM : thm list -> string list * thm list (* Definitional CNF *)
63 val FOL_NORM_TTAC : (string list * thm list -> tactic) -> thm list -> tactic