Stream: Mirror: Isabelle Development Mailing List

Topic: instantiate_laws.py in AFP entry Registers

Email Gateway (Mar 11 2026 at 12:47):

From: Florian Haftmann <florian.haftmann@cit.tum.de>

While doing some maintenance, I stumbled over

https://foss.heptapod.net/isa-afp/afp-devel/-/blob/branch/default/thys/Registers/instantiate_laws.py?ref_type=heads

What is the status of this tool?

Since it is obviously needed to maintain the entry, it is a little bit
odd that it is not implemented in one of the established languages and
e.g. integrated as a regular Isabelle tool.

Florian

OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc

Last updated: Mar 17 2026 at 17:04 UTC