[isabelle-dev] isabelle-dev and ML files

Timothy Bourke Timothy.Bourke at nicta.com.au
Fri Oct 23 02:30:29 CEST 2009

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

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

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?


-------------- 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>

More information about the isabelle-dev mailing list