Re: [isabelle] Numeral is acting strangely



On Wed, 5 Jul 2006, Jeremy Dawson wrote:

> > read "Numeral1";
> val it = Const ("Numeral.Numeral1", "'a::Numeral.number") : Term.term
> 
> So Numeral1 is a constant in its own right

> But here the constant "Numeral.Numeral1" somehow gets translated to
> number_of (Numeral.Pls BIT bit.B1)

You seem to using a recent development snapshot.  Here Numeral1 is a
first-class term abbreviation, i.e. it may appear as a Const at some
point, but is expanded eventually (during term certification at the
latest).

Your read ML function seems to refer to rather old internal interfaces,
based on Sign.read_def_terms. Try ProofContext.read_term to get the usual
user-level thing.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.