equal
deleted
inserted
replaced
11 signature DATATYPE_TACTICS = |
11 signature DATATYPE_TACTICS = |
12 sig |
12 sig |
13 val induct_tac: string -> int -> tactic |
13 val induct_tac: string -> int -> tactic |
14 val exhaust_tac: string -> int -> tactic |
14 val exhaust_tac: string -> int -> tactic |
15 val rep_datatype_i: thm -> thm -> thm list -> thm list -> theory -> theory |
15 val rep_datatype_i: thm -> thm -> thm list -> thm list -> theory -> theory |
16 val rep_datatype: thmref * Args.src list -> thmref * Args.src list -> |
16 val rep_datatype: thmref * Attrib.src list -> thmref * Attrib.src list -> |
17 (thmref * Args.src list) list -> (thmref * Args.src list) list -> theory -> theory |
17 (thmref * Attrib.src list) list -> (thmref * Attrib.src list) list -> theory -> theory |
18 val setup: (theory -> theory) list |
18 val setup: (theory -> theory) list |
19 end; |
19 end; |
20 |
20 |
21 |
21 |
22 (** Datatype information, e.g. associated theorems **) |
22 (** Datatype information, e.g. associated theorems **) |