equal
deleted
inserted
replaced
74 (* Construction of a term from a list of Preterms *) |
74 (* Construction of a term from a list of Preterms *) |
75 val list_mk_abs : (term list * term) -> term |
75 val list_mk_abs : (term list * term) -> term |
76 val list_mk_imp : (term list * term) -> term |
76 val list_mk_imp : (term list * term) -> term |
77 val list_mk_forall : (term list * term) -> term |
77 val list_mk_forall : (term list * term) -> term |
78 val list_mk_conj : term list -> term |
78 val list_mk_conj : term list -> term |
79 val list_mk_disj : term list -> term |
|
80 |
79 |
81 (* Destructing a term to a list of Preterms *) |
80 (* Destructing a term to a list of Preterms *) |
82 val strip_comb : term -> (term * term list) |
81 val strip_comb : term -> (term * term list) |
83 val strip_abs : term -> (term list * term) |
82 val strip_abs : term -> (term list * term) |
84 val strip_imp : term -> (term list * term) |
83 val strip_imp : term -> (term list * term) |