equal
deleted
inserted
replaced
25 val morph_fp_sugar: morphism -> fp_sugar -> fp_sugar |
25 val morph_fp_sugar: morphism -> fp_sugar -> fp_sugar |
26 val fp_sugar_of: Proof.context -> string -> fp_sugar option |
26 val fp_sugar_of: Proof.context -> string -> fp_sugar option |
27 |
27 |
28 val tvar_subst: theory -> typ list -> typ list -> ((string * int) * typ) list |
28 val tvar_subst: theory -> typ list -> typ list -> ((string * int) * typ) list |
29 val exists_subtype_in: typ list -> typ -> bool |
29 val exists_subtype_in: typ list -> typ -> bool |
|
30 val flat_rec: ('a -> 'b list) -> 'a list -> 'b list |
30 val mk_co_iter: theory -> BNF_FP_Util.fp_kind -> typ -> typ list -> term -> term |
31 val mk_co_iter: theory -> BNF_FP_Util.fp_kind -> typ -> typ list -> term -> term |
31 val nesty_bnfs: Proof.context -> typ list list list -> typ list -> BNF_Def.bnf list |
32 val nesty_bnfs: Proof.context -> typ list list list -> typ list -> BNF_Def.bnf list |
32 val indexify_fst: ''a list -> (int -> ''a * 'b -> 'c) -> ''a * 'b -> 'c |
33 val indexify_fst: ''a list -> (int -> ''a * 'b -> 'c) -> ''a * 'b -> 'c |
33 val mk_un_fold_co_rec_prelims: BNF_FP_Util.fp_kind -> typ list -> typ list -> int list -> |
34 val mk_un_fold_co_rec_prelims: BNF_FP_Util.fp_kind -> typ list -> typ list -> int list -> |
34 int list list -> term list -> term list -> Proof.context -> |
35 int list list -> term list -> term list -> Proof.context -> |