Re: [isabelle] Here's 54 ML_file imports from SML/NJ Library; fix regexp-lib.sml if you'd like



On Thu, 17 Apr 2014, Lawrence Paulson wrote:

It is possible that Isabelle’s own libraries modify some of these things (Char possibly), creating incompatibilities with the SML Basis Library.

See also http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2013-2/src/Pure/ML-Systems/proper_int.ML

  SML basis with type int representing proper integers, not machine words.

Isabelle/ML is not Standard ML, it is what Standard ML could have been if that had not been messed up in the late 1990-ies.


If you want to continue this regexp comilation experiment seriously, you should probably move over to isabelle-dev and do it as a test for the forthcoming SML IDE, which integrates official SML into the Isabelle environment.

That might require some further adjustments of these relatively new things, but that is then part of the continuous development process over there.


	Makarius


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.