On Wed, 7 May 2014, Johannes Hölzl wrote:
* Theorems about complex numbers are now stated only using Re and Im, the
Complex
constructor is not used anymore. It is possible to use primcorec to defined the
behaviour of a complex-valued function.
This is also a surprising application of primcorec!
That is indeed very nice. Is that a new invention or an old trick that
every category theorist knows?
In mathematics books / lectures there is usually some handwaving only, to
justify why it is possible to define functions on complex by specifying
the observation of Re/Im.
Makarius_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
