Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] access axclass data

view this post on Zulip 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

view this post on Zulip 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: Nov 21 2024 at 12:39 UTC