[isabelle] undocumented command: permanent_interpretation

I just stumbled about the command

and could not find any documentation in isar-ref.
As usual, the ML-source code gives no documentation, too, except
the command description: 
  "prove interpretation of locale expression into named theory"

So what does this command do, and how does it differ from
interpretation, and why isn't it documented, but used inside HOL
sessions (E.g., IMP)?


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.