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.