Alicia (Feb 20 2026 at 00:52): Alicia (Feb 20 2026 at 00:52):Hello, we came across #Archive Mirror: Isabelle Users Mailing List > [isabelle] parametric typedef?.
Could you explain the last part about instantiating an underspecified constant in more depth? Thanks in advance!
Lukas Stevens (Feb 20 2026 at 09:18):I think Makarius might be referring to this paper: https://ebjohnsen.org/publication/06-njc/06-njc.pdf
Lukas Stevens (Feb 20 2026 at 09:57):Theory instantiation is not something that exists in the Isabelle distribution. There is, however, local theory instantiation through locales. There, the restriction discussed in the thread applies, though.
Last updated: Feb 27 2026 at 20:31 UTC