Josh Chen

Tactics looping on Isabelle2021

1

Certain tactics loop on [Isabelle2021-RC3](https://isabelle.sketis.net/website-Isabelle2021-RC3/). Needs further investigation.

Pure equality vs defined definitional equality

1

The theory thus far has been written to use the built-in Pure equality as the definitional equality, the idea initially being to take advantage of as much built-in functionality as...

Can we include (or export) plugins for numbering, labels and references?

5

I'm throwing together a collection of plugins to provide LaTeX-style functionality for theorem (lemma/definition/remark...) and equation labels and referencing, as well as for section numbering (the former integrates with, but...