[isabelle-dev] NEWS: avoid the Complex constructor, use the more natural Re/Im view

[Makarius]

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