9 sig |
9 sig |
10 val to_set_att: thm list -> attribute |
10 val to_set_att: thm list -> attribute |
11 val to_pred_att: thm list -> attribute |
11 val to_pred_att: thm list -> attribute |
12 val to_pred : thm list -> Context.generic -> thm -> thm |
12 val to_pred : thm list -> Context.generic -> thm -> thm |
13 val pred_set_conv_att: attribute |
13 val pred_set_conv_att: attribute |
14 val add_inductive_i: |
14 val add_inductive: |
15 Inductive.inductive_flags -> |
15 Inductive.flags -> |
16 ((binding * typ) * mixfix) list -> |
16 ((binding * typ) * mixfix) list -> |
17 (string * typ) list -> |
17 (string * typ) list -> |
18 (Attrib.binding * term) list -> thm list -> |
18 (Attrib.binding * term) list -> thm list -> |
19 local_theory -> Inductive.inductive_result * local_theory |
19 local_theory -> Inductive.result * local_theory |
20 val add_inductive: bool -> bool -> |
20 val add_inductive_cmd: bool -> bool -> |
21 (binding * string option * mixfix) list -> |
21 (binding * string option * mixfix) list -> |
22 (binding * string option * mixfix) list -> |
22 (binding * string option * mixfix) list -> |
23 Specification.multi_specs_cmd -> (Facts.ref * Token.src list) list -> |
23 Specification.multi_specs_cmd -> (Facts.ref * Token.src list) list -> |
24 local_theory -> Inductive.inductive_result * local_theory |
24 local_theory -> Inductive.result * local_theory |
25 val mono_add: attribute |
25 val mono_add: attribute |
26 val mono_del: attribute |
26 val mono_del: attribute |
27 end; |
27 end; |
28 |
28 |
29 structure Inductive_Set: INDUCTIVE_SET = |
29 structure Inductive_Set: INDUCTIVE_SET = |
516 ({intrs = intrs', elims = elims', induct = induct, inducts = inducts, |
516 ({intrs = intrs', elims = elims', induct = induct, inducts = inducts, |
517 raw_induct = raw_induct', preds = map fst defs, eqs = eqs'}, |
517 raw_induct = raw_induct', preds = map fst defs, eqs = eqs'}, |
518 lthy4) |
518 lthy4) |
519 end; |
519 end; |
520 |
520 |
521 val add_inductive_i = Inductive.gen_add_inductive_i add_ind_set_def; |
|
522 val add_inductive = Inductive.gen_add_inductive add_ind_set_def; |
521 val add_inductive = Inductive.gen_add_inductive add_ind_set_def; |
|
522 val add_inductive_cmd = Inductive.gen_add_inductive_cmd add_ind_set_def; |
523 |
523 |
524 fun mono_att att = |
524 fun mono_att att = |
525 Thm.declaration_attribute (fn thm => fn context => |
525 Thm.declaration_attribute (fn thm => fn context => |
526 Thm.attribute_declaration att (to_pred [] context thm) context); |
526 Thm.attribute_declaration att (to_pred [] context thm) context); |
527 |
527 |