[isabelle-dev] Suc 0 necessary?

[Chris Capel]

translations
  "1" <= "Suc 0"
  "2" <= "Suc (Suc 0)"

Is there a reason why the above isn't defined by default? Is it a
matter of preference? Context? As a translation, the above doesn't
interfere with simplification machinery, so I don't think including it
by default would do any harm. Of course, not including it would be
fine too. But in the latter case perhaps the statement could be
mentioned in documentation instead of the current apology for the
strangeness of seeing "Suc 0" where one would expect "1".

The 2 translation isn't as important. It seems like I occasionally see
"Suc (Suc 0)", but I don't think the simplifier will ever leave it.

Chris Capel
-- 
"What is it like to be a bat? What is it like to bat a bee? What is it
like to be a bee being batted? What is it like to be a batted bee?"
-- The Mind's I (Hofstadter, Dennet)