1 theory Nominal2

     1 theory Nominal2

     2 imports 

     2 imports 

     3   Nominal2_Base Nominal2_Abs Nominal2_FCB

     3   Nominal2_Base Nominal2_Abs Nominal2_FCB

     4 keywords

     4 keywords

     5   "nominal_datatype" :: thy_decl and

     5   "nominal_datatype" :: thy_decl and

     7   "avoids" "binds"

     7   "avoids" "binds"

     8 begin

     8 begin

     9 

     9 

    10 ML_file "nominal_dt_data.ML"

    10 ML_file "nominal_dt_data.ML"

    11 ML {* open Nominal_Dt_Data *}

    11 ML {* open Nominal_Dt_Data *}