Here, is the collection of neighborhoods of zero (sets whose interior contains the neutral element of the group), and for two sets we define as .
Also, I replaced jsMath with MathJax as the LaTeX rendering engine on the isarmathlib.org site. The results are very good, the math renders faster and it looks better. It forced me to do some Haskell programming again to modify the tool that parses Isar and generates HTML with LaTeX markup. I haven’t seen that code or programmed in Haskell for about two years, but with Leksah now in Ubuntu repositories it was rather easy: just modify the code in one place and keep fixing it until it builds. Once it built, it worked.
The tool will probably become obsolete after the next Isabelle release. There is a Google Summer of Code project that will allow generating nice HTML presentations of Isar theories from within Isabelle.