[isabelle] Congruence rules for the code preprocessor



Hi,

the code generator tutorial mentions that "the simpset for the code preprocessor can apply the full generality of the Isabelle simplifier". But how can I add anything else other than unfold theorems? The attributes code_unfold and code_inline do not accept declarations like

declare conj_cong[code_inline cong]

Is there a way in Isar to declare congruence rules to the preprocessor?

Regards,
Andreas





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