1857 in |
1857 in |
1858 timer; |
1858 timer; |
1859 ({Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, xtor_un_folds = folds, |
1859 ({Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, xtor_un_folds = folds, |
1860 xtor_co_recs = recs, xtor_co_induct = ctor_induct_thm, |
1860 xtor_co_recs = recs, xtor_co_induct = ctor_induct_thm, |
1861 xtor_strong_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms, |
1861 xtor_strong_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms, |
1862 ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, map_thms = folded_ctor_map_thms, |
1862 ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, |
1863 set_thmss = folded_ctor_set_thmss', rel_thms = ctor_Irel_thms, |
1863 xtor_map_thms = folded_ctor_map_thms, xtor_set_thmss = folded_ctor_set_thmss', |
1864 xtor_un_fold_thms = ctor_fold_thms, xtor_co_rec_thms = ctor_rec_thms}, |
1864 xtor_rel_thms = ctor_Irel_thms, xtor_un_fold_thms = ctor_fold_thms, |
|
1865 xtor_co_rec_thms = ctor_rec_thms}, |
1865 lthy |> Local_Theory.notes (common_notes @ notes) |> snd) |
1866 lthy |> Local_Theory.notes (common_notes @ notes) |> snd) |
1866 end; |
1867 end; |
1867 |
1868 |
1868 val _ = |
1869 val _ = |
1869 Outer_Syntax.local_theory @{command_spec "datatype_new"} "define BNF-based inductive datatypes" |
1870 Outer_Syntax.local_theory @{command_spec "datatype_new"} "define BNF-based inductive datatypes" |