Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Abstract Substitution

Email Gateway (Oct 04 2024 at 08:40):

From: "Thiemann, René" <cl-isabelle-users@lists.cam.ac.uk>
Dear all,

I’d like to announce a new AFP entry:

Abstract Substitution
by Martin Desharnais

Abstract:
This entry provides a small, reusable, theory that specifies the abstract
concept of substition as monoid action. Both the substitution type and the
object type are kept abstract. The theory provides multiple useful definitions
and lemmas. Two example usages are provided for first order terms: one for terms
from the AFP/First_Order_Terms session and one for terms from the
Isabelle/HOL-ex session.

https://www.isa-afp.org/entries/Abstract_Substitution.html

Enjoy,
René

Last updated: Jan 04 2025 at 20:18 UTC