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
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

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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