[isabelle] ML code in Isar files




Using the latest development version of Isabelle,
I have Isar files thus:

...

ML {*
...

val _ = bind_thms ("word_arith_nat_defs", map dop fas2) ;

...

 ... =   ... word_arith_nat_defs ...

*}

Now when the semicolon in the above is omitted, the code fails with a message

Value or constructor (word_arith_nat_defs) has not been declared

When the semicolon is replaced the code works fine.

Can anyone tell why this is?

Thanks,

Jeremy Dawson







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