[isabelle-dev] New analysis material

[Fabian Immler]

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 [1] (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 
amorphous HOL-Analysis.

Fabian


[1] 
https://ci.isabelle.systems/jenkins/job/isabelle-all/ws/browser_info/HOL/HOL-Analysis/manual.pdf

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5581 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20190322/6e5cfc88/attachment.bin>