equal
deleted
inserted
replaced
62 val mk_iterate : term * term * term -> term; |
62 val mk_iterate : term * term * term -> term; |
63 val mk_fail : term; |
63 val mk_fail : term; |
64 val mk_return : term -> term; |
64 val mk_return : term -> term; |
65 val list_ccomb : term * term list -> term; |
65 val list_ccomb : term * term list -> term; |
66 val con_app2 : string -> ('a -> term) -> 'a list -> term; |
66 val con_app2 : string -> ('a -> term) -> 'a list -> term; |
|
67 val prj : ('a -> 'b -> 'a) -> ('a -> 'b -> 'a) -> 'a -> 'b list -> int -> 'a |
67 val proj : term -> 'a list -> int -> term; |
68 val proj : term -> 'a list -> int -> term; |
68 val mk_ctuple_pat : term list -> term; |
69 val mk_ctuple_pat : term list -> term; |
69 val mk_branch : term -> term; |
70 val mk_branch : term -> term; |
70 |
71 |
71 (* Creating propositions *) |
72 (* Creating propositions *) |