> 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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
