equal
deleted
inserted
replaced
6 *) |
6 *) |
7 |
7 |
8 signature AX_CLASS = |
8 signature AX_CLASS = |
9 sig |
9 sig |
10 val define_class: bstring * class list -> string list -> |
10 val define_class: bstring * class list -> string list -> |
11 ((binding * attribute list) * term list) list -> theory -> class * theory |
11 (Thm.binding * term list) list -> theory -> class * theory |
12 val add_classrel: thm -> theory -> theory |
12 val add_classrel: thm -> theory -> theory |
13 val add_arity: thm -> theory -> theory |
13 val add_arity: thm -> theory -> theory |
14 val prove_classrel: class * class -> tactic -> theory -> theory |
14 val prove_classrel: class * class -> tactic -> theory -> theory |
15 val prove_arity: string * sort list * sort -> tactic -> theory -> theory |
15 val prove_arity: string * sort list * sort -> tactic -> theory -> theory |
16 val get_info: theory -> class -> |
16 val get_info: theory -> class -> |