Re: [isabelle] code_include in Isabelle2014?

Hi Thomas,

This is now subsumed by code_printing with the category code_module.

code_printing code_module <name of the module> \<rightharpoonup> (<language>) {*<text>*}


On 11/09/14 11:32, Thomas Genet wrote:

Dear all,

is there a replacement command for "code_include" that was present in Isabelle2012 (at

I did not see anything about this in the cumulative NEWS on Isabelle versions.

Thanks in advance,


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