[isabelle] Code generation for "int" in Isabelle 2013-1 RC3



Dear all,

the code generation snippet in the attached file worked in Isabelle
2013 but fails in Isabelle 2013-1 RC3; a function resembling the SML
Vector.findi (http://www.standardml.org/Basis/vector.html) is
introduced in Isabelle, and then serialised to SML Vector.findi, but
apparently there is a clash between the Isabelle code generated
structure "int" and the SML "IntInf.int".

I have tried to import "Code_Target_Int" with similar result.

Is there an easy way to avoid such clash? (I could edit the SML code
by hand and fix types' declarations, but does not seem a proper
solution).

Thanks in advance for any advice,

Jesus

Attachment: IArray_findi.thy
Description: Binary data



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