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.

Andreas

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
String.thy: http://isabelle.in.tum.de/reports/Isabelle/rev/0a3fa8fbcdc5

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.

	Florian


--
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.edu
http://pp.info.uni-karlsruhe.de
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.