Email Gateway (Aug 17 2022 at 13:45): Email Gateway (Aug 17 2022 at 13:45):From: Makarius <makarius@sketis.net>
Since SML is not oo, there is nothing like a public method, of course.
Nevertheless, AxClass.print_axclasses is already a good guess. If you
look at the sources in Pure/axclass.ML, just the next line after the
declaration of print_axclasses is this:
val get_info: theory -> string -> {super_classes: class list, intro:
thm, axioms: thm list}
Makarius
Email Gateway (Aug 17 2022 at 13:45):From: Sean McLaughlin <seanmcl@cmu.edu>
Hello,
I'd like to programatically access axclass data, such as axioms and
super classes.
It seems that access to the type axclass_info would do, and this is
used in the
public method "AxClass.print_axclasses", yet I can't figure out how
to get at it.
I believe it's part of the Sign.sg. Is it possible?
Thanks,
Sean
Last updated: May 03 2024 at 04:19 UTC