Re: [isabelle] Rational numbers in Isabelle/ML

However, I would imagine that the exported could would be quite ugly.
*The exported /code/

Also, I just remembered another issue that should be taken care of: As far as I'm aware, there is currently no way to convert HOL rational numbers to Isabelle/ML rational numbers and the other way round. (like what I do in MyRat)

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