equal
deleted
inserted
replaced
7 signature TYPE_INFER = |
7 signature TYPE_INFER = |
8 sig |
8 sig |
9 val is_param: indexname -> bool |
9 val is_param: indexname -> bool |
10 val is_paramT: typ -> bool |
10 val is_paramT: typ -> bool |
11 val param: int -> string * sort -> typ |
11 val param: int -> string * sort -> typ |
|
12 val mk_param: int -> sort -> typ |
12 val anyT: sort -> typ |
13 val anyT: sort -> typ |
13 val paramify_vars: typ -> typ |
14 val paramify_vars: typ -> typ |
14 val paramify_dummies: typ -> int -> typ * int |
15 val paramify_dummies: typ -> int -> typ * int |
15 val deref: typ Vartab.table -> typ -> typ |
16 val deref: typ Vartab.table -> typ -> typ |
16 val finish: Proof.context -> typ Vartab.table -> typ list * term list -> typ list * term list |
17 val finish: Proof.context -> typ Vartab.table -> typ list * term list -> typ list * term list |