[isabelle-dev] neg_numeral fallout

[Lars Noschinski]

On 17.05.2014 17:33, Florian Haftmann wrote:
>> See now 376604d56b5
> http://isabelle.in.tum.de/reports/Isabelle/rev/376604d56b54
>
> The changeset is misleading since it describes »- 1« as special case of
> a numeral, which it is not (any longer) – it is just the canonical
> representation of minus one.
I considered it as special as "1" (as we don't have any rules to
transform -1 to 1 in this context). What would you have preferred
instead? Or is this about "-1" instead of "- 1"?

  -- Lars