Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/Nominal2.thy
changeset 2885 1264f2a21ea9
parent 2868 2b8e387d2dfc
child 2886 d7066575cbb9
equal deleted inserted replaced
2884:0599286b1e2a 2885:1264f2a21ea9 
     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")
 
    13 begin
 
    14 begin
 
       
    15 
       
    16 use "nominal_dt_data.ML"
 
       
    17 ML {* open Nominal_Dt_Data *}
 
    14 
    18 
    15 use "nominal_dt_rawfuns.ML"
 
    19 use "nominal_dt_rawfuns.ML"
 
    16 ML {* open Nominal_Dt_RawFuns *}
 
    20 ML {* open Nominal_Dt_RawFuns *}
 
    17 
    21 
    18 use "nominal_dt_alpha.ML"
 
    22 use "nominal_dt_alpha.ML"
 
   137 end
 
   141 end
 
   138 *}
 
   142 *}
 
   139 
   143 
   140 
   144 
   141 ML {*
 
   145 ML {*
 
       
   146 (* definition of the raw datatype *)
 
       
   147 
   142 fun define_raw_dts dts bn_funs bn_eqs bclauses lthy =
 
   148 fun define_raw_dts dts bn_funs bn_eqs bclauses lthy =
 
   143 let
 
   149 let
 
   144   val thy = Local_Theory.exit_global lthy
 
   150   val thy = Local_Theory.exit_global lthy
 
   145   val thy_name = Context.theory_name thy
 
   151   val thy_name = Context.theory_name thy
 
   146 
   152 
   457   val thms_name = 
   463   val thms_name = 
   458     the_default (Binding.name (space_implode "_" qty_names)) opt_thms_name 
   464     the_default (Binding.name (space_implode "_" qty_names)) opt_thms_name 
   459   fun thms_suffix s = Binding.qualified true s thms_name 
   465   fun thms_suffix s = Binding.qualified true s thms_name 
   460   val case_names_attr = Attrib.internal (K (Rule_Cases.case_names cnstr_names))
 
   466   val case_names_attr = Attrib.internal (K (Rule_Cases.case_names cnstr_names))
 
   461 
   467 
       
   468   val infos = mk_infos qty_full_names qeq_iffs' qdistincts qstrong_exhaust_thms qstrong_induct_thms
 
       
   469 
   462   val (_, lthy9') = lthyC
 
   470   val (_, lthy9') = lthyC
 
       
   471      |> Local_Theory.declaration false (K (fold register_info infos))
 
   463      |> Local_Theory.note ((thms_suffix "distinct", [induct_attr, simp_attr]), qdistincts) 
   472      |> Local_Theory.note ((thms_suffix "distinct", [induct_attr, simp_attr]), qdistincts) 
   464      ||>> Local_Theory.note ((thms_suffix "eq_iff", [induct_attr, simp_attr]), qeq_iffs')
 
   473      ||>> Local_Theory.note ((thms_suffix "eq_iff", [induct_attr, simp_attr]), qeq_iffs')
 
   465      ||>> Local_Theory.note ((thms_suffix "fv_defs", []), qfv_defs) 
   474      ||>> Local_Theory.note ((thms_suffix "fv_defs", []), qfv_defs) 
   466      ||>> Local_Theory.note ((thms_suffix "bn_defs", []), qbn_defs) 
   475      ||>> Local_Theory.note ((thms_suffix "bn_defs", []), qbn_defs) 
   467      ||>> Local_Theory.note ((thms_suffix "perm_simps", [eqvt_attr, simp_attr]), qperm_simps) 
   476      ||>> Local_Theory.note ((thms_suffix "perm_simps", [eqvt_attr, simp_attr]), qperm_simps)
nominal2