[isabelle-dev] New analysis material
immler at in.tum.de
Fri Mar 22 18:19:11 CET 2019
On 3/22/2019 8:51 AM, Lawrence Paulson wrote:
> But we can easily see a pattern now, with more or less abstract
topology being developed before integration theory, complex analysis,
winding numbers and other horrors. This may suggest a division of
Analysis, maybe even before the next release.
I would like to take the opportunity to advertise this observation as a
success of the efforts of everyone who contributed to tagging HOL-Analysis.
The resulting document  (e.g. for isabelle/35ba13ac6e5c) helped to
clarify the dependencies of a lot of (elementary) material that was
hidden in between "other horrors" and sort it into the right places
(currently chapter 1-4).
I believe this helped Larry to install the new material into appropriate
places such that we can now see a bit more structure in the previously
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 5581 bytes
Desc: S/MIME Cryptographic Signature
More information about the isabelle-dev