changeset 15706 | bc264e730103 |
parent 15703 | 727ef1b8b3ee |
child 16123 | 1381e90c2694 |
15705:b5edb9dcec9a | 15706:bc264e730103 |
---|---|
478 val setup = [Attrib.add_attributes [("ind_realizer", |
478 val setup = [Attrib.add_attributes [("ind_realizer", |
479 (rlz_attrib_global, K Attrib.undef_local_attribute), |
479 (rlz_attrib_global, K Attrib.undef_local_attribute), |
480 "add realizers for inductive set")]]; |
480 "add realizers for inductive set")]]; |
481 |
481 |
482 end; |
482 end; |
483 |