[isabelle-dev] New analysis material
lp15 at cam.ac.uk
Mon Mar 25 12:10:22 CET 2019
I didn’t use the document, but I certainly noticed the new theories. I always try to put material as close to the root of the tree as possible.
> On 22 Mar 2019, at 17:19, Fabian Immler <immler at in.tum.de> wrote:
> 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 amorphous HOL-Analysis.
>  https://ci.isabelle.systems/jenkins/job/isabelle-all/ws/browser_info/HOL/HOL-Analysis/manual.pdf
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev