equal
deleted
inserted
replaced
34 |
34 |
35 val morph_ctr_sugar: morphism -> ctr_sugar -> ctr_sugar |
35 val morph_ctr_sugar: morphism -> ctr_sugar -> ctr_sugar |
36 val transfer_ctr_sugar: Proof.context -> ctr_sugar -> ctr_sugar |
36 val transfer_ctr_sugar: Proof.context -> ctr_sugar -> ctr_sugar |
37 val ctr_sugar_of: Proof.context -> string -> ctr_sugar option |
37 val ctr_sugar_of: Proof.context -> string -> ctr_sugar option |
38 val ctr_sugars_of: Proof.context -> ctr_sugar list |
38 val ctr_sugars_of: Proof.context -> ctr_sugar list |
|
39 val register_ctr_sugar: string -> ctr_sugar -> local_theory -> local_theory |
39 |
40 |
40 val rep_compat_prefix: string |
41 val rep_compat_prefix: string |
41 |
42 |
42 val mk_half_pairss: 'a list * 'a list -> ('a * 'a) list list |
43 val mk_half_pairss: 'a list * 'a list -> ('a * 'a) list list |
43 val join_halves: int -> 'a list list -> 'a list list -> 'a list * 'a list list list |
44 val join_halves: int -> 'a list list -> 'a list list -> 'a list * 'a list list list |