[isabelle-dev] Gromov Hyperbolicity

Tobias Nipkow nipkow at in.tum.de
Thu Jan 18 08:32:01 CET 2018

For those of you interested in formalization of Analysis


I would like to call your attention to this entry because it is rich in concepts 
and theorems that are more general than the actual focus of the article. I 
believe quite a bit of the material could be pulled out and made more visible. 
Here are some pointers:

1. Library/Complement contains both new generic material like "t3_space" but 
also new concepts like [mono_intros] for more automation in proving of 
inequalities. In short, there is a wealth of material that might be suitable for 
inclusion in HOL-Analysis.
I have already made a start by moving a few [simp] rules but that is it from me 
because I am not familiar enough with the Analysis material.

2. Hausdorff_Dinstance, Metric_Completion and Isometries stronly smell of 
generic concepts that should go somewhere else.
We need a discussion on whether any of the theories deserve a separate AFP entry.

Sebbastien has already made an effort to separate the generic from the specific. 
We should capitalize on that, but it needs a bit of voluntary work.


-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5156 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20180118/f8debb5a/attachment.p7s>

More information about the isabelle-dev mailing list