14 val get_all_info: Proof.context -> (string * info) list |
14 val get_all_info: Proof.context -> (string * info) list |
15 val get_info: Proof.context -> string -> info option |
15 val get_info: Proof.context -> string -> info option |
16 val the_info: Proof.context -> string -> info |
16 val the_info: Proof.context -> string -> info |
17 val register_info: (string * info) -> Context.generic -> Context.generic |
17 val register_info: (string * info) -> Context.generic -> Context.generic |
18 val mk_infos: string list -> thm list -> thm list -> thm list -> thm list -> (string * info) list |
18 val mk_infos: string list -> thm list -> thm list -> thm list -> thm list -> (string * info) list |
|
19 |
|
20 datatype alpha_result = AlphaResult of |
|
21 {alpha_names : string list, |
|
22 alpha_trms : term list, |
|
23 alpha_tys : typ list, |
|
24 alpha_bn_names : string list, |
|
25 alpha_bn_trms : term list, |
|
26 alpha_bn_tys : typ list, |
|
27 alpha_intros : thm list, |
|
28 alpha_cases : thm list, |
|
29 alpha_raw_induct : thm} |
|
30 |
19 end |
31 end |
20 |
32 |
21 structure Nominal_Dt_Data: NOMINAL_DT_DATA = |
33 structure Nominal_Dt_Data: NOMINAL_DT_DATA = |
22 struct |
34 struct |
|
35 |
23 |
36 |
24 (* information generated by nominal_datatype *) |
37 (* information generated by nominal_datatype *) |
25 type info = |
38 type info = |
26 {inject : thm list, |
39 {inject : thm list, |
27 distinct : thm list, |
40 distinct : thm list, |
53 }) |
66 }) |
54 in |
67 in |
55 map aux ty_names |
68 map aux ty_names |
56 end |
69 end |
57 |
70 |
|
71 datatype alpha_result = AlphaResult of |
|
72 {alpha_names : string list, |
|
73 alpha_trms : term list, |
|
74 alpha_tys : typ list, |
|
75 alpha_bn_names : string list, |
|
76 alpha_bn_trms : term list, |
|
77 alpha_bn_tys : typ list, |
|
78 alpha_intros : thm list, |
|
79 alpha_cases : thm list, |
|
80 alpha_raw_induct : thm} |
|
81 |
58 |
82 |
59 end |
83 end |