[isabelle-dev] Recent instabilities of HOL-Decision_Procs

[Makarius]

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