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-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev