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. 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. Larry _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
