Notification Bot (Mar 25 2026 at 11:56): Notification Bot (Mar 25 2026 at 11:56):Ant S. has marked this topic as resolved.
Chelsea Edmonds (Mar 26 2026 at 08:10):Just an add on as the question itself has already been answered perfectly but I just noticed this today - were you referencing my course on Modular Proofs in Isabelle/HOL at MGS25 by any chance? If so, one its great to see it still getting used! Feel free to message me if you have any feedback, as I've been thinking about building on this to create an extended locales tutorial at some point :) And two, worth noting that the more algebraic examples were often adapted from the official locales/type classes tutorials (linked in the slides), so you might find it useful to use both the course resources and the official tutorials in parallel.
Last updated: Apr 14 2026 at 09:21 UTC