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. Larry
> On 22 Mar 2019, at 17:19, Fabian Immler <[email protected]> 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 [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 > > _______________________________________________ > isabelle-dev mailing list > [email protected] > https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
