[isabelle-dev] Merge-Sort Implementation
bulwahn at in.tum.de
Thu Oct 27 17:13:23 CEST 2011
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
> 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
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
It is seems feasible to get rid of the Random engine if one can replace
these occurrences by something else appropriate.
More information about the isabelle-dev