8      ("nominal_inductive.ML")

     8      ("nominal_inductive.ML")

     9      ("nominal_function_common.ML")

     9      ("nominal_function_common.ML")

    10      ("nominal_function_core.ML")

    10      ("nominal_function_core.ML")

    11      ("nominal_mutual.ML")

    11      ("nominal_mutual.ML")

    12      ("nominal_function.ML")

    12      ("nominal_function.ML")

    13      ("nominal_dt_data.ML")

    14      ("nominal_dt_data.ML")

    14 begin

    15 begin

    15 

    16 

    16 use "nominal_dt_data.ML"

    17 use "nominal_dt_data.ML"

    17 ML {* open Nominal_Dt_Data *}

    18 ML {* open Nominal_Dt_Data *}

    42 (* for defining nominal functions      *)

    43 (* for defining nominal functions      *)

    43 use "nominal_function_common.ML"

    44 use "nominal_function_common.ML"

    44 use "nominal_function_core.ML"

    45 use "nominal_function_core.ML"

    45 use "nominal_mutual.ML"

    46 use "nominal_mutual.ML"

    46 use "nominal_function.ML"

    47 use "nominal_function.ML"

    47 

    49 

    48 ML {*

    50 ML {*

    49 val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add)

    51 val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add)

    50 val rsp_attr = Attrib.internal (K Quotient_Info.rsp_rules_add)

    52 val rsp_attr = Attrib.internal (K Quotient_Info.rsp_rules_add)

    51 val simp_attr = Attrib.internal (K Simplifier.simp_add)

    53 val simp_attr = Attrib.internal (K Simplifier.simp_add)