Email Gateway (Aug 19 2022 at 17:00): Email Gateway (Aug 19 2022 at 17:00):From: Peter Lammich <lammich@in.tum.de>
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)?
Email Gateway (Aug 19 2022 at 17:02):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
This will be an official, documented part of the next Isabelle release.
Its infamous predecessor has been around since 2010 and seems to have
done a good job in escaping broader attention so far ;-).
Florian
signature.asc
Last updated: Apr 18 2024 at 08:19 UTC