[isabelle-dev] [isabelle] power2_sum outside of rings
lp15 at cam.ac.uk
Wed Jun 22 21:21:30 CEST 2011
As I recall, the number class is for all types where numerals have a meaning. Of course, it is a constituent of number_ring, to which many numeric types belong, but not the naturals.
On 22 Jun 2011, at 19:55, Florian Haftmann wrote:
>> A more drastic solution would be to just get rid of the "number" class
>> altogether (its sole purpose seems to be so that you can have types
>> where numerals have a non-standard meaning) and have a single
>> definition of number_of that works uniformly for all types.
> This would indeed be helpful, but I guess the natural numbers are the
> show stopper.
> Of course we could also attempt to get rid of signed numerals ;-)
> PGP available:
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev