[isabelle] setsum.cong as fundef_cong


I noticed that setsum.cong, setprod.cong etc. are not declared as fundef_cong. This is important for function-package function definitions where a recursive call occurs under a setsum or setprod. Without these declarations.

Is there a reason not to put these declarations into Groups_Big? If not, is it unproblematic to simply add the declaration to the cong lemma in the locale comm_monoid_set, or should only setsum.cong and setprod.cong be declared as fundef_cong rules explicitly?



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.