Re: [isabelle] String.explode in generated code

Hi Florian,

thanks for figuring this out. I will keep your code_modulename workaround until I switch to the development version again.


Florian Haftmann schrieb:
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.


Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 023
76131 Karlsruhe

Telefon: +49 721 608-48352
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft

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