Le mercredi 8 juin 2016 14:01:32 UTC+2, Stephan Merz a écrit :- I believe the requirement that successor be injective is missing in the Peano axioms as they are given in Specifying Systems, and I added it to the definition of natural numbers that underlies the Isabelle backend of
TLAPS.