41 |
41 |
42 ML {* |
42 ML {* |
43 val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add) |
43 val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add) |
44 val rsp_attr = Attrib.internal (K Quotient_Info.rsp_rules_add) |
44 val rsp_attr = Attrib.internal (K Quotient_Info.rsp_rules_add) |
45 val simp_attr = Attrib.internal (K Simplifier.simp_add) |
45 val simp_attr = Attrib.internal (K Simplifier.simp_add) |
|
46 val induct_attr = Attrib.internal (K Induct.induct_simp_add) |
46 *} |
47 *} |
47 |
48 |
48 section{* Interface for nominal_datatype *} |
49 section{* Interface for nominal_datatype *} |
49 |
50 |
50 ML {* print_depth 50 *} |
51 ML {* print_depth 50 *} |
453 the_default (Binding.name (space_implode "_" qty_names)) opt_thms_name |
454 the_default (Binding.name (space_implode "_" qty_names)) opt_thms_name |
454 fun thms_suffix s = Binding.qualified true s thms_name |
455 fun thms_suffix s = Binding.qualified true s thms_name |
455 val case_names_attr = Attrib.internal (K (Rule_Cases.case_names cnstr_names)) |
456 val case_names_attr = Attrib.internal (K (Rule_Cases.case_names cnstr_names)) |
456 |
457 |
457 val (_, lthy9') = lthyC |
458 val (_, lthy9') = lthyC |
458 |> Local_Theory.note ((thms_suffix "distinct", []), qdistincts) |
459 |> Local_Theory.note ((thms_suffix "distinct", [induct_attr, simp_attr]), qdistincts) |
459 ||>> Local_Theory.note ((thms_suffix "eq_iff", []), qeq_iffs') |
460 ||>> Local_Theory.note ((thms_suffix "eq_iff", [induct_attr, simp_attr]), qeq_iffs') |
460 ||>> Local_Theory.note ((thms_suffix "fv_defs", []), qfv_defs) |
461 ||>> Local_Theory.note ((thms_suffix "fv_defs", []), qfv_defs) |
461 ||>> Local_Theory.note ((thms_suffix "bn_defs", []), qbn_defs) |
462 ||>> Local_Theory.note ((thms_suffix "bn_defs", []), qbn_defs) |
462 ||>> Local_Theory.note ((thms_suffix "perm_simps", [eqvt_attr, simp_attr]), qperm_simps) |
463 ||>> Local_Theory.note ((thms_suffix "perm_simps", [eqvt_attr, simp_attr]), qperm_simps) |
463 ||>> Local_Theory.note ((thms_suffix "fv_bn_eqvt", []), qfv_qbn_eqvts) |
464 ||>> Local_Theory.note ((thms_suffix "fv_bn_eqvt", []), qfv_qbn_eqvts) |
464 ||>> Local_Theory.note ((thms_suffix "size", []), qsize_simps) |
465 ||>> Local_Theory.note ((thms_suffix "size", []), qsize_simps) |