equal
deleted
inserted
replaced
24 val get_all_info: Proof.context -> (string * info) list |
24 val get_all_info: Proof.context -> (string * info) list |
25 val get_info: Proof.context -> string -> info option |
25 val get_info: Proof.context -> string -> info option |
26 val the_info: Proof.context -> string -> info |
26 val the_info: Proof.context -> string -> info |
27 val register_info: (string * info) -> Context.generic -> Context.generic |
27 val register_info: (string * info) -> Context.generic -> Context.generic |
28 val mk_infos: string list -> thm list -> thm list -> thm list -> thm list -> (string * info) list |
28 val mk_infos: string list -> thm list -> thm list -> thm list -> thm list -> (string * info) list |
|
29 |
|
30 datatype user_data = UserData of |
|
31 {dts : dt_info, |
|
32 cn_names : string list, |
|
33 cn_tys : (string * string) list, |
|
34 bn_funs : (binding * typ * mixfix) list, |
|
35 bn_eqs : (Attrib.binding * term) list, |
|
36 bclauses : bclause list list list} |
29 |
37 |
30 datatype raw_dt_info = RawDtInfo of |
38 datatype raw_dt_info = RawDtInfo of |
31 {raw_dt_names : string list, |
39 {raw_dt_names : string list, |
32 raw_dts : dt_info, |
40 raw_dts : dt_info, |
33 raw_tys : typ list, |
41 raw_tys : typ list, |
110 in |
118 in |
111 map aux ty_names |
119 map aux ty_names |
112 end |
120 end |
113 |
121 |
114 |
122 |
|
123 datatype user_data = UserData of |
|
124 {dts : dt_info, |
|
125 cn_names : string list, |
|
126 cn_tys : (string * string) list, |
|
127 bn_funs : (binding * typ * mixfix) list, |
|
128 bn_eqs : (Attrib.binding * term) list, |
|
129 bclauses : bclause list list list} |
|
130 |
115 datatype raw_dt_info = RawDtInfo of |
131 datatype raw_dt_info = RawDtInfo of |
116 {raw_dt_names : string list, |
132 {raw_dt_names : string list, |
117 raw_dts : dt_info, |
133 raw_dts : dt_info, |
118 raw_tys : typ list, |
134 raw_tys : typ list, |
119 raw_ty_args : (string * sort) list, |
135 raw_ty_args : (string * sort) list, |