[isabelle-dev] NEWS

[Tobias Nipkow]

Thank you for this, Florian. The one thing I had hoped for when I initiated
this change was that one can write "n-1" just like "n+1", but that doesn't
quite work yet, probably because you have some special syntax for what used to
be negative numerals. This may ease the conversion, but can we get rid of it
eventually?

Tobias


Am 19/11/2013 18:18, schrieb Florian Haftmann:
> This refers to Isabelle/e7c9a14632d0 and AFP/797f66d26443.
> 
> * Abolished neg_numeral. * Canonical representation for minus one is "-
> 1". * Canonical representation for other negative numbers is "- (numeral
> _)". * When devising rule sets for number calculation, consider the 
> following cases: 0, 1, numeral _, - 1, - numeral _. * Syntax for negative
> numerals is mere input syntax. INCOMPATBILITY.
> 
> This is definitely a non-trivial change with has been conceived only after
> some – partly experimental – iterations.  Experts and stakeholders in the
> numeral area are strongly encouraged to comment.
> 
> Florian
> 
> 
> 
> _______________________________________________ isabelle-dev mailing list 
> isabelle-dev at in.tum.de 
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>