Nominal/Nominal2.thy
changeset 3201 3e6f4320669f
parent 3190 1b7c034c9e9e
child 3214 13ab4f0a0b0e
equal deleted inserted replaced
3200:995d47b09ab4 3201:3e6f4320669f
     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
     6   "nominal_primrec" "nominal_inductive" :: thy_goal and
     6   "nominal_primrec" "nominal_inductive" :: thy_goal and
     7   "avoids" "binds"
     7   "avoids" "binds"
     8 uses ("nominal_dt_rawfuns.ML")
       
     9      ("nominal_dt_alpha.ML")
       
    10      ("nominal_dt_quot.ML")
       
    11      ("nominal_induct.ML")
       
    12      ("nominal_inductive.ML")
       
    13      ("nominal_function_common.ML")
       
    14      ("nominal_function_core.ML")
       
    15      ("nominal_mutual.ML")
       
    16      ("nominal_function.ML")
       
    17      ("nominal_termination.ML")
       
    18      ("nominal_dt_data.ML")
       
    19 begin
     8 begin
    20 
     9 
    21 use "nominal_dt_data.ML"
    10 ML_file "nominal_dt_data.ML"
    22 ML {* open Nominal_Dt_Data *}
    11 ML {* open Nominal_Dt_Data *}
    23 
    12 
    24 use "nominal_dt_rawfuns.ML"
    13 ML_file "nominal_dt_rawfuns.ML"
    25 ML {* open Nominal_Dt_RawFuns *}
    14 ML {* open Nominal_Dt_RawFuns *}
    26 
    15 
    27 use "nominal_dt_alpha.ML"
    16 ML_file "nominal_dt_alpha.ML"
    28 ML {* open Nominal_Dt_Alpha *}
    17 ML {* open Nominal_Dt_Alpha *}
    29 
    18 
    30 use "nominal_dt_quot.ML"
    19 ML_file "nominal_dt_quot.ML"
    31 ML {* open Nominal_Dt_Quot *}
    20 ML {* open Nominal_Dt_Quot *}
    32 
    21 
    33 (*****************************************)
    22 (*****************************************)
    34 (* setup for induction principles method *)
    23 (* setup for induction principles method *)
    35 use "nominal_induct.ML"
    24 ML_file "nominal_induct.ML"
    36 method_setup nominal_induct =
    25 method_setup nominal_induct =
    37   {* NominalInduct.nominal_induct_method *}
    26   {* NominalInduct.nominal_induct_method *}
    38   {* nominal induction *}
    27   {* nominal induction *}
    39 
    28 
    40 (****************************************************)
    29 (****************************************************)
    41 (* inductive definition involving nominal datatypes *)
    30 (* inductive definition involving nominal datatypes *)
    42 use "nominal_inductive.ML" 
    31 ML_file "nominal_inductive.ML" 
    43 
    32 
    44 
    33 
    45 (***************************************)
    34 (***************************************)
    46 (* forked code of the function package *)
    35 (* forked code of the function package *)
    47 (* for defining nominal functions      *)
    36 (* for defining nominal functions      *)
    48 use "nominal_function_common.ML"
    37 ML_file "nominal_function_common.ML"
    49 use "nominal_function_core.ML"
    38 ML_file "nominal_function_core.ML"
    50 use "nominal_mutual.ML"
    39 ML_file "nominal_mutual.ML"
    51 use "nominal_function.ML"
    40 ML_file "nominal_function.ML"
    52 use "nominal_termination.ML"
    41 ML_file "nominal_termination.ML"
    53 
    42 
    54 ML {*
    43 ML {*
    55 val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add)
    44 val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add)
    56 val simp_attr = Attrib.internal (K Simplifier.simp_add)
    45 val simp_attr = Attrib.internal (K Simplifier.simp_add)
    57 val induct_attr = Attrib.internal (K Induct.induct_simp_add)
    46 val induct_attr = Attrib.internal (K Induct.induct_simp_add)