[isabelle-dev] NumeralSyntax.mk_bin
Walther Neuper
neuper at ist.tugraz.at
Wed Aug 26 12:43:03 CEST 2009
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
Thanks a lot in advance,
Walther
PS: Please, just direct me to some reading, in case this question is too
elementary.
--
------------------------------------------------------------------------
Walther Neuper Mailto: neuper at ist.tugraz.at
Institute for Software Technology Tel: +43-(0)316/873-5728
University of Technology Fax: +43-(0)316/873-5706
Graz, Austria Home: www.ist.tugraz.at/neuper
------------------------------------------------------------------------
More information about the isabelle-dev
mailing list