equal
deleted
inserted
replaced
8 signature AX_CLASS = |
8 signature AX_CLASS = |
9 sig |
9 sig |
10 val add_thms_as_axms: (string * thm) list -> theory -> theory |
10 val add_thms_as_axms: (string * thm) list -> theory -> theory |
11 val add_classrel_thms: thm list -> theory -> theory |
11 val add_classrel_thms: thm list -> theory -> theory |
12 val add_arity_thms: thm list -> theory -> theory |
12 val add_arity_thms: thm list -> theory -> theory |
13 val add_axclass: rclass * xclass list -> (string * string) list |
13 val add_axclass: bclass * xclass list -> (string * string) list |
14 -> theory -> theory |
14 -> theory -> theory |
15 val add_axclass_i: rclass * class list -> (string * term) list |
15 val add_axclass_i: bclass * class list -> (string * term) list |
16 -> theory -> theory |
16 -> theory -> theory |
17 val add_inst_subclass: xclass * xclass -> string list -> thm list |
17 val add_inst_subclass: xclass * xclass -> string list -> thm list |
18 -> tactic option -> theory -> theory |
18 -> tactic option -> theory -> theory |
19 val add_inst_subclass_i: class * class -> string list -> thm list |
19 val add_inst_subclass_i: class * class -> string list -> thm list |
20 -> tactic option -> theory -> theory |
20 -> tactic option -> theory -> theory |