[isabelle-dev] [isabelle] power2_sum outside of rings

[Lawrence Paulson]

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.
Larry

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 ;-)
> 
> 	Florian
> 
> -- 
> 
> Home:
> http://www.in.tum.de/~haftmann
> 
> PGP available:
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev