Some generated code is attached to objects like in ``` ProductType in Class with attribute eancode : String rule mrule1_s89024694_29_generated : $ forall x/ProductType (not (Isa(x,Product))) ==> (x ISA Product) $; mrule4_s89024694_34_generated : $ forall x/Proposition (Isa(x,Product)) ==> (x in ProductType) $ end ``` The implementation just check whether the attribute label ends with 'generated'. This disallows attributes that have the simple label 'generated' or 'hasgenerated'. The check in Propositions2Pragment should be more specific to only mark generated attribute labels.