localeisabelleinterpretation

Isabelle resolves interpretation


I'm using Isabelle 2019 and got some troubles regarding locals:

I'm constructing a locale with an abbrevation, e.g.:

interpretation myInstance : myLocale "abbreviation"

I'm using this with a function from the locale, e.g.:

myInstance.getter myinput

But apply simp now "simplifies" the goal to something like this

myLocale.getter "abbreviation" myinput

How can I avoid simp to do this? (I'm pretty sure, this is the reason, why my code takes ages to process)...

Best


Solution

  • This is a known issue and there is no perfect solution. Some partial solutions: