[isabelle-dev] Suc 0 necessary?

[Tobias Nipkow]

> Doesn't it make sense to leave it to users to decide which 
> representation they want? Is there really any convincing reason why "1 = 
> Suc 0" needs to be a simp rule?

IIRC, 1 used to abbreviate Suc 0. Making "1 = Suc 0" a simp rule mimiced 
that. It allows you to write 1 on the rhs of an equation because (if 
used as a simp rule) the 1 will be replaced by Suc 0. Of course this 
does not work on the lhs...

Even if we did not make "1 = Suc 0" a simp rule, we would still need to 
decide how to phrase the library theorems. This would still bias the user.

Tobias