23 val the_info: Proof.context -> string -> info |
23 val the_info: Proof.context -> string -> info |
24 val register_info: (string * info) -> Context.generic -> Context.generic |
24 val register_info: (string * info) -> Context.generic -> Context.generic |
25 val mk_infos: string list -> thm list -> thm list -> thm list -> thm list -> (string * info) list |
25 val mk_infos: string list -> thm list -> thm list -> thm list -> thm list -> (string * info) list |
26 |
26 |
27 datatype user_data = UserData of |
27 datatype user_data = UserData of |
28 {dts : Datatype.spec list, |
28 {dts : Old_Datatype.spec list, |
29 cn_names : string list, |
29 cn_names : string list, |
30 cn_tys : (string * string) list, |
30 cn_tys : (string * string) list, |
31 bn_funs : (binding * typ * mixfix) list, |
31 bn_funs : (binding * typ * mixfix) list, |
32 bn_eqs : (Attrib.binding * term) list, |
32 bn_eqs : (Attrib.binding * term) list, |
33 bclauses : bclause list list list} |
33 bclauses : bclause list list list} |
34 |
34 |
35 datatype raw_dt_info = RawDtInfo of |
35 datatype raw_dt_info = RawDtInfo of |
36 {raw_dt_names : string list, |
36 {raw_dt_names : string list, |
37 raw_dts : Datatype.spec list, |
37 raw_dts : Old_Datatype.spec list, |
38 raw_tys : typ list, |
38 raw_tys : typ list, |
39 raw_ty_args : (string * sort) list, |
39 raw_ty_args : (string * sort) list, |
40 raw_cns_info : cns_info list, |
40 raw_cns_info : cns_info list, |
41 raw_all_cns : term list list, |
41 raw_all_cns : term list list, |
42 raw_inject_thms : thm list, |
42 raw_inject_thms : thm list, |
109 map aux ty_names |
109 map aux ty_names |
110 end |
110 end |
111 |
111 |
112 |
112 |
113 datatype user_data = UserData of |
113 datatype user_data = UserData of |
114 {dts : Datatype.spec list, |
114 {dts : Old_Datatype.spec list, |
115 cn_names : string list, |
115 cn_names : string list, |
116 cn_tys : (string * string) list, |
116 cn_tys : (string * string) list, |
117 bn_funs : (binding * typ * mixfix) list, |
117 bn_funs : (binding * typ * mixfix) list, |
118 bn_eqs : (Attrib.binding * term) list, |
118 bn_eqs : (Attrib.binding * term) list, |
119 bclauses : bclause list list list} |
119 bclauses : bclause list list list} |
120 |
120 |
121 datatype raw_dt_info = RawDtInfo of |
121 datatype raw_dt_info = RawDtInfo of |
122 {raw_dt_names : string list, |
122 {raw_dt_names : string list, |
123 raw_dts : Datatype.spec list, |
123 raw_dts : Old_Datatype.spec list, |
124 raw_tys : typ list, |
124 raw_tys : typ list, |
125 raw_ty_args : (string * sort) list, |
125 raw_ty_args : (string * sort) list, |
126 raw_cns_info : cns_info list, |
126 raw_cns_info : cns_info list, |
127 raw_all_cns : term list list, |
127 raw_all_cns : term list list, |
128 raw_inject_thms : thm list, |
128 raw_inject_thms : thm list, |