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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
