[isabelle-dev] NumeralSyntax.mk_bin

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Wed Aug 26 13:54:13 CEST 2009

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

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

More information about the isabelle-dev mailing list