4 uses ("nominal_dt_rawfuns.ML")

     4 uses ("nominal_dt_rawfuns.ML")

     5      ("nominal_dt_alpha.ML")

     5      ("nominal_dt_alpha.ML")

     6      ("nominal_dt_quot.ML")

     6      ("nominal_dt_quot.ML")

     7      ("nominal_induct.ML")

     7      ("nominal_induct.ML")

     8      ("nominal_inductive.ML")

     8      ("nominal_inductive.ML")

     9      ("nominal_function_core.ML")

    10      ("nominal_function_core.ML")

    10      ("nominal_mutual.ML")

    11      ("nominal_mutual.ML")

    11      ("nominal_function.ML")

    12      ("nominal_function.ML")

    12 begin

    13 begin

    13 

    14 

    33 

    34 

    34 

    35 

    35 (***************************************)

    36 (***************************************)

    36 (* forked code of the function package *)

    37 (* forked code of the function package *)

    37 (* for defining nominal functions      *)

    38 (* for defining nominal functions      *)

    38 use "nominal_function_core.ML"

    40 use "nominal_function_core.ML"

    39 use "nominal_mutual.ML"

    41 use "nominal_mutual.ML"

    40 use "nominal_function.ML"

    42 use "nominal_function.ML"

    41 

    43 

    42 ML {*

    44 ML {*