[isabelle-dev] Merge-Sort Implementation

[Lukas Bulwahn]

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.


Lukas