[isabelle-dev] New analysis material
nipkow at in.tum.de
Sat Mar 23 08:08:58 CET 2019
Same as Fabian, I am very happy that this tagging exercise (which entailed a
certain amount of restructuring) helped. The real test will be the envisaged
split of Analysis into smaller sessions.
On 22/03/2019 18:19, Fabian Immler 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
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 5581 bytes
Desc: S/MIME Cryptographic Signature
More information about the isabelle-dev