[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