[isabelle-dev] neg_numeral fallout
noschinl at in.tum.de
Mon May 19 10:41:19 CEST 2014
On 17.05.2014 17:33, Florian Haftmann wrote:
>> See now 376604d56b5
> 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"?
More information about the isabelle-dev