[isabelle-dev] Complex.thy

[Tobias Nipkow]

On 20/11/2019 17:36, Manuel Eberl wrote:
> On the other hand, I'm not sure what your exact plans for restructuring are, but 
> I thought we were going to have some session that contains complex number and 
> the basic operations on them but not integration.

Fabian had proposed to move Complex out and I agree with that. Uless we follow 
some established set of books (I had suggested Bourbaki a long while back...) we 
need some clear cut criterion that is easy to realize. This one is.

Tobias

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5579 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20191120/1f925d85/attachment.bin>