[isabelle-dev] Recent instabilities of HOL-Decision_Procs

Makarius makarius at sketis.net
Wed Sep 8 15:51:44 CEST 2010

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.


More information about the isabelle-dev mailing list