On Mon, 6 Sep 2010, Johannes Hölzl wrote:
Attached is the code generated by Approximate_Ex line 42. I generated it
by using ML {* ML_Context.trace := true *}. I also added some functions
from integer.ML to work properly on pure polyml.
The result needs to contain:
val res = true : bool
when the computation was successfully.
Excellent. I could reproduce the issue in isolation here. I will wrap up
shortly, and send a report to David Matthews off-list.
Makarius_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
