Re: [isabelle] String.explode in generated code

Hi again,

> After some experimentation I have a feeling that code_reserved does not
> exactly behave as expected, I will keep track on this.

the reason for this »misbevahiour« were the following lines added to

E.g. they would fix the module name »String«.

I am not able to reconstruct was my motivation was to add these, but now
they are removed for good.




PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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