[isabelle-dev] Merge-Sort Implementation

[Makarius]

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.


 	Makarius