[isabelle-dev] Complex.thy

[Tobias Nipkow]

On 20/11/2019 16:20, Lawrence Paulson wrote:
> As a small experiment, I tried moving this theory from the main HOL directory to Analysis. I discovered a number of minor, unexpected dependencies:
> 
> Library/OptionalSugar.thy: There is code to hide coercions, surely unnecessary since we have had implicit coercions for years.

It is necessary because the coercions are printed. But removing the complex bits 
is no problem.

> Library/Nonpos_Ints.thy: There is material relating these primitives to the complex numbers, which could easily be moved to Complex.thy.
> 
> Computational_Algebra/Formal_Power_Series.thy: There are references to i. These could be harder to deal with.
> 
> I suppose that we can leave things as they are, but it seems weird to introduce an absolutely minimal signature of the complex numbers in one place and then the basics much later in Analysis.

I would prefer the latter.

Tobias

> Larry
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
> 

-------------- 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/99c1aa39/attachment.bin>