search

SKolodynski / IsarMathLib

IsarMathLib is a library of formalized mathematics for Isabelle/ZF.
https://isarmathlib.org
Other
16 stars 2 forks source link

TopologicalGroup_ZF.thy HTML rendering broken for v1.12.0 #7

Closed SKolodynski closed 4 years ago

SKolodynski commented 4 years ago

The isar2html tool cannot parse TopologicalGroup_ZF.thy released with v1.12.0 so it can not be presented at isarmathlib.org.

dan323 commented 4 years ago

What is the specific issue?

SKolodynski commented 4 years ago

There are some Isar constructs that you are using that are not supported by isar2html parser. I don't want you to worry too much about that, so far I could always modify the proofs to not use them. In this specific case there were missing comments before theorems (isar2html enforces this) and constructs like group0.group0_5_L2(2)[OF group0_valid_in_tgroup, of g] that the isar2html parser does not accept. When I was fixing this I got some ideas on how to shorten the proofs of the lemmas you have added, you can see the changes in the commit.