[isabelle] ML code in Isar files
- To: isabelle-users at cl.cam.ac.uk
- Subject: [isabelle] ML code in Isar files
- From: Jeremy Dawson <Jeremy.Dawson at rsise.anu.edu.au>
- Date: Thu, 05 Jul 2007 10:46:11 +1000
- In-reply-to: <Pine.LNX.email@example.com>
- Organization: Australian National University
- References: <Pine.LNX.4.64.0706230255010.7173@cvx> <Pine.LNX.firstname.lastname@example.org>
- User-agent: Thunderbird 18.104.22.168 (X11/20070306)
Using the latest development version of Isabelle,
I have Isar files thus:
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
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and