[isabelle-dev] isabelle-dev and ML files

[Timothy Bourke]

I'm having some trouble working with ML files in recent dev versions.

Given, for example, a file test.ML:
  structure Test =
  struct
    val s1 = "\<top>";
    val s2 = "\\<top>";
  end;

And two tests:
  ML) Direct ML: isabelle-process < test.ML
 USE) Interactive isabelle: use "test.ML";

I get the following results for Isabelle 2009 and a recent (yesterday)
dev version:
      \            version
  test \     2009          dev
        +-------------+------------+
    ML  |  s1 fails   |  s1 fails  |
        |  s2 works   |  s2 works  |
        +-------------+------------+
    USE |  s1 works   |  s1 works  |
        |  s2 works   |  s2 fails  |
        +-------------+------------+

Is the dev behaviour correct?

Tim.

-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 187 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20091023/f19368be/attachment.sig>