equal
deleted
inserted
replaced
30 type basic_lfp_sugar = |
30 type basic_lfp_sugar = |
31 {T: typ, |
31 {T: typ, |
32 fp_res_index: int, |
32 fp_res_index: int, |
33 C: typ, |
33 C: typ, |
34 fun_arg_Tsss : typ list list list, |
34 fun_arg_Tsss : typ list list list, |
35 ctr_defs: thm list, |
|
36 ctr_sugar: Ctr_Sugar.ctr_sugar, |
35 ctr_sugar: Ctr_Sugar.ctr_sugar, |
37 recx: term, |
36 recx: term, |
38 rec_thms: thm list}; |
37 rec_thms: thm list}; |
39 |
38 |
40 type lfp_rec_extension = |
39 type lfp_rec_extension = |
107 type basic_lfp_sugar = |
106 type basic_lfp_sugar = |
108 {T: typ, |
107 {T: typ, |
109 fp_res_index: int, |
108 fp_res_index: int, |
110 C: typ, |
109 C: typ, |
111 fun_arg_Tsss : typ list list list, |
110 fun_arg_Tsss : typ list list list, |
112 ctr_defs: thm list, |
|
113 ctr_sugar: ctr_sugar, |
111 ctr_sugar: ctr_sugar, |
114 recx: term, |
112 recx: term, |
115 rec_thms: thm list}; |
113 rec_thms: thm list}; |
116 |
114 |
117 type lfp_rec_extension = |
115 type lfp_rec_extension = |