Email Gateway (Jan 12 2023 at 14:17): Email Gateway (Jan 12 2023 at 14:17):From: Qiyuan XU ????? <cl-isabelle-users@lists.cam.ac.uk>
Dear Isabelle users,
In local_theory.ML, Local_Theory.declaration has two arguments, syntax and pervasive.
I know this interface is used to declare any data change so that local theories like locales can replay the data change. It is a way to add state change in locales.
But what I don't know is the meaning of the two arguments. Is there anyone can help me about this?
Thank you.
Qiyuan Xu
CONFIDENTIALITY: This email is intended solely for the person(s) named and may be confidential and/or privileged. If you are not the intended recipient, please delete it, notify us and do not copy, use, or disclose its contents.
Towards a sustainable earth: Print only when necessary. Thank you.
Email Gateway (Jan 18 2023 at 16:35):From: Makarius <makarius@sketis.net>
See the "isar-ref" manual section 5.6 on "Generic declarations" --- it is
about the Isar command 'declaration'.
Moreover, you should look at typical example applications, either of the Isar
command or the ML function behind it.
Makarius
Last updated: Apr 19 2024 at 16:20 UTC