equal
deleted
inserted
replaced
1022 |
1022 |
1023 subsection {* Configuration of the code generator *} |
1023 subsection {* Configuration of the code generator *} |
1024 |
1024 |
1025 code_datatype "0::'a::zero poly" pCons |
1025 code_datatype "0::'a::zero poly" pCons |
1026 |
1026 |
|
1027 declare pCons_0_0 [code post] |
|
1028 |
1027 instantiation poly :: ("{zero,eq}") eq |
1029 instantiation poly :: ("{zero,eq}") eq |
1028 begin |
1030 begin |
1029 |
1031 |
1030 definition [code del]: |
1032 definition [code del]: |
1031 "eq_class.eq (p::'a poly) q \<longleftrightarrow> p = q" |
1033 "eq_class.eq (p::'a poly) q \<longleftrightarrow> p = q" |