Re: [isabelle] OCaml code generator problem: Big_int



Florian Haftmann wrote:
> Hi Peter,
>
>   
>> the Ocaml code generator generates the following lines of (invalid)
>> OCaml-Code. Note that I'm using Efficient_Nat:
>>     
>
> this deficiency did not come to surface before the release of Isabelle
> 2009.  A solution is to replace src/HOL/Library/Efficient_Nat.thy by
> http://www4.in.tum.de/~haftmann/resources/Efficient_Nat.thy.
>
> Hope this helps
> 	Florian
>
>   
Thank you very much, this helped!
The generated Ocaml code now compiles.

Regards
  Peter





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