<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<p><font size="+1">The references to i in Formal_Power_Series are
restricted to a very small and simple (almost trivial) set of
theorems that are completely disconnected from everything else
in there. They are about the relationship between sin, cos, tan,
and exp as formal power series and I'm pretty sure they're not
used anywhere in the distribution or the AFP (a quick grep seems
to confirm that). They're certainly relevant, but I see no
problem in moving them somewhere else.</font></p>
<p><font size="+1">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. Then
Computational_Algebra could import that. Or perhaps Complex
could import Computational_Algebra (not sure if that makes
sense). But as I said, I also don't see a problem with simply
moving those few theorems out of Formal_Power_Series.</font></p>
<p><font size="+1">Manuel<br>
</font></p>
<p><font size="+1"><br>
</font></p>
<div class="moz-cite-prefix">On 20/11/2019 16:41, Tobias Nipkow
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:a12151bd-583c-cba4-a9ef-4fe134b2d3f8@in.tum.de">
<br>
<br>
On 20/11/2019 16:20, Lawrence Paulson wrote:
<br>
<blockquote type="cite">As a small experiment, I tried moving this
theory from the main HOL directory to Analysis. I discovered a
number of minor, unexpected dependencies:
<br>
<br>
Library/OptionalSugar.thy: There is code to hide coercions,
surely unnecessary since we have had implicit coercions for
years.
<br>
</blockquote>
<br>
It is necessary because the coercions are printed. But removing
the complex bits is no problem.
<br>
<br>
<blockquote type="cite">Library/Nonpos_Ints.thy: There is material
relating these primitives to the complex numbers, which could
easily be moved to Complex.thy.
<br>
<br>
Computational_Algebra/Formal_Power_Series.thy: There are
references to i. These could be harder to deal with.
<br>
<br>
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.
<br>
</blockquote>
<br>
I would prefer the latter.
<br>
<br>
Tobias
<br>
<br>
<blockquote type="cite">Larry
<br>
<br>
_______________________________________________
<br>
isabelle-dev mailing list
<br>
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<br>
<a class="moz-txt-link-freetext" href="https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev">https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev</a>
<br>
<br>
</blockquote>
<br>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<pre class="moz-quote-pre" wrap="">_______________________________________________
isabelle-dev mailing list
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<a class="moz-txt-link-freetext" href="https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev">https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev</a>
</pre>
</blockquote>
</body>
</html>