Re: [isabelle] access axclass data



On Sun, 8 Jan 2006, Sean McLaughlin wrote:

> 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"

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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.