[isabelle-dev] NumeralSyntax.mk_bin

[Florian Haftmann]

Hi Walter,

> Why is NumeralSyntax.setup available in HOL/Int.thy, but not in the
> Isabelle/HOL ML toplevel ? ...
> 
> ML> NumeralSyntax.setup;
> Error-Structure (NumeralSyntax) has not been declared   Found near
> NumeralSyntax.setup

the reason for this is that Isabelle administrates the ML name space on
its own as soon as the Pure bootstrap is finished.  That is, ML that is
compiled under the control of Isabelle (which is the default!) is not
available from the raw ML toplevel.

Usually it is best to test ML snippets within a regular Isar session, e.g.

$ isabelle tty
> theory Foo imports Main begin;
> ML {* NumeralSyntax.setup *};


Hope this helps
	Florian

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 252 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20090826/bc550541/attachment.sig>