[isabelle-dev] Merge-Sort Implementation

Makarius makarius at sketis.net
Thu Oct 27 17:23:32 CEST 2011

On Thu, 27 Oct 2011, Lukas Bulwahn wrote:

> On 10/27/2011 04:38 PM, Florian Haftmann wrote:
>>> Nonetheless, we still have the real-based Library.random from "ML for
>>> the working programmer", because without it quickcheck performs really
>>> bad.
>> AFAIR this has only been the case for the ancient SML quickcheck,
>> whereas my quickcheck implementation comes with a random generator in
>> HOL based on a cousin in Haskell.  If this is true, we could throw away
>> Library.random.  Maybe Lukas can comment on this.
> What Florian mentioned is correct.
> A closer code inspection tells me:
> Matrix/Compute_Oracle/am_sml.ML still uses it to get a unique identifier, 
> probably this can be replaced by a more standard serial_string ()
> Slegdehammer uses it to randomly announce information from Geoff Sutcliffe to 
> our users.
> Mutabelle has another copy of a Random engine for some random-choice 
> function.
> It is seems feasible to get rid of the Random engine if one can replace 
> these occurrences by something else appropriate.

The above occurrences are sufficient to substantiate it remaining in the 
library.  There is no real problem with it anymore.


More information about the isabelle-dev mailing list