[isabelle] Congruence rules for the code preprocessor


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?


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