For those of you interested in formalization of Analysis
https://devel.isa-afp.org/entries/Gromov_Hyperbolicity.htmlI 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.
Tobias
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
