Email Gateway (May 29 2022 at 08:09): Email Gateway (May 29 2022 at 08:09):From: Leo Freitas <leo.freitas@newcastle.ac.uk>
Hello,
Is there a command to list the set of theorems named from a particular attribute (i.e. like print_simpset but for other named_theorems name sets)? I tried looking into Pure and how it defines print_simpset but it didn’t seem obvious from within attrib.ML.
The use case is that I am trying to create various lists of named_theorems attributes in order to control (as much as possible) the proof of a VDM theorem translated to Isabelle. In most cases, it’s a matter of specific simplifications over the “right” set, which is determined by the VDM to Isabelle translation process.
Is there any reference (or suggestion) on how to construct (and inspect) such lists?
Many thanks,
Leo
Email Gateway (May 29 2022 at 09:55):From: Peter Lammich <lammich@in.tum.de>
Hi
You can just use the thm command.
thm yourCollection
Prints all theorems in the list.
For more control over simpsets, you might want to have a look at the
named_simpset command ( which is not in Isabelle distrib though)
https://www21.in.tum.de/~lammich/isabelle_llvm/Isabelle_LLVM/Named_Simpsets.html
.. Peter
Last updated: Apr 19 2024 at 20:15 UTC