3105 map2 (fn b => fn thms => |
3105 map2 (fn b => fn thms => |
3106 ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])) |
3106 ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])) |
3107 bs thmss) |
3107 bs thmss) |
3108 in |
3108 in |
3109 timer; |
3109 timer; |
3110 ({Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors, un_folds = unfolds, co_recs = corecs, |
3110 ({Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors, xtor_un_folds = unfolds, |
3111 co_induct = dtor_coinduct_thm, strong_co_induct = dtor_strong_coinduct_thm, |
3111 xtor_co_recs = corecs, xtor_co_induct = dtor_coinduct_thm, |
3112 dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, |
3112 xtor_strong_co_induct = dtor_strong_coinduct_thm, dtor_ctors = dtor_ctor_thms, |
|
3113 ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, |
3113 map_thms = folded_dtor_map_thms, set_thmss = folded_dtor_set_thmss', |
3114 map_thms = folded_dtor_map_thms, set_thmss = folded_dtor_set_thmss', |
3114 rel_thms = dtor_Jrel_thms, un_fold_thms = ctor_dtor_unfold_thms, |
3115 rel_thms = dtor_Jrel_thms, xtor_un_fold_thms = ctor_dtor_unfold_thms, |
3115 co_rec_thms = ctor_dtor_corec_thms}, |
3116 xtor_co_rec_thms = ctor_dtor_corec_thms}, |
3116 lthy |> Local_Theory.notes (common_notes @ notes) |> snd) |
3117 lthy |> Local_Theory.notes (common_notes @ notes) |> snd) |
3117 end; |
3118 end; |
3118 |
3119 |
3119 val _ = |
3120 val _ = |
3120 Outer_Syntax.local_theory @{command_spec "codatatype"} "define BNF-based coinductive datatypes" |
3121 Outer_Syntax.local_theory @{command_spec "codatatype"} "define BNF-based coinductive datatypes" |