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
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
