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 [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
