Email Gateway (Aug 18 2022 at 10:37): Email Gateway (Aug 18 2022 at 10:37):From: Jeremy Dawson <Jeremy.Dawson@rsise.anu.edu.au>
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
Last updated: May 03 2024 at 12:27 UTC