[isabelle] undocumented command: permanent_interpretation



I just stumbled about the command
  permanent_interpretation

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)?


--
  Peter





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