Lines Matching refs:list
24 val traceBack : varmap -> term_bdd list -> thm -> thm -> (term_bdd * (term_bdd * term_bdd) list) list
28 val flatten_pair : term -> term list
29 val BddSatone : term_bdd -> (term_bdd * term_bdd) list
31 val findTrace : varmap -> thm -> thm -> thm -> thm * thm list * thm
34 val computeTrace : (int -> term_bdd -> 'a) -> varmap -> thm -> thm * thm -> term_bdd list
39 val BddSubst : (term_bdd * term_bdd) list -> term_bdd -> term_bdd
42 val extendVarmap : term list -> varmap -> varmap
44 val showVarmap : unit -> (string * int) list
49 val extendSat : term list -> varmap -> (term_bdd * term_bdd) list -> (term_bdd * term_bdd) list
52 val split_subst : (term_bdd * term_bdd) list -> (term_bdd * term_bdd) list * (term_bdd * term_bdd) list