| changeset 20380 | 14f9f2a1caa6 |
| parent 19008 | 14c1b2f5dda4 |
| child 20588 | c847c56edf0c |
| 20379:154d8c155a65 | 20380:14f9f2a1caa6 |
|---|---|
225 val Part_Collect = thm "Part_Collect"; |
225 val Part_Collect = thm "Part_Collect"; |
226 |
226 |
227 val basic_monos = thms "basic_monos"; |
227 val basic_monos = thms "basic_monos"; |
228 *} |
228 *} |
229 |
229 |
230 subsection {* Codegenerator setup *} |
|
231 |
|
232 code_alias |
|
233 "+" "Sum_Type.sum" |
|
234 "Inr" "Sum_Type.Inr" |
|
235 "Inl" "Sum_Type.Inl" |
|
236 |
|
237 end |
230 end |