IsarMathLib 1.22.1: Update to Isabelle2021-1

This release updates IsarMathLib to Isabelle2021-1. There was actually not much to update – only a couple of places in the informal text that referenced Isabelle2021 now reference Isabelle2021-1. The main difference is in the HTML presentation that Isabelle generates from IsarMathLib sources. This presentation improved somewhat and now has links to referenced theorems in proofs. In one respect it is even better than the presentation at the isarmathlib.org site – the locale names in the statements of theorems are linked to the definitions, which is a feature missing on isarmathlib.org. I remember some statements by Makarius Wentzel on the Isabelle mailing list that the goal is the “publication quality” of officially generated HTML presentation. I hope that this includes what I think is needed the most – folding of structured proofs, support for mathematical notation with custom symbols and options for reduction of syntactic noise so that characters like the question mark or the quotes separating the object logic statements are omitted. When this happens I would be happy to retire the tool that generates isarmathlib.org HTML files. I wrote that tool 14 years ago with only a scant knowledge of HTML, CSS or Java Script and the web pages it generates are probably hopelessly old-style.

In other news, Pedro Sánchez Terraf announced that his team has completed a formalization of the independence of CH in Isabelle/ZF. This is a good news for IsarMathLib as well. Isabelle/ZF is used by very few people and I worry that at some point the Isabelle team stops supporting it, which would be the end of IsarMathLib. Every application like this makes it less likely.

Advertisement

Tags: , ,

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

This site uses Akismet to reduce spam. Learn how your comment data is processed.


%d bloggers like this: