1852 (*FIXME: once the package exports all the necessary high-level characteristic theorems, |
1852 (*FIXME: once the package exports all the necessary high-level characteristic theorems, |
1853 those should not only be concealed but rather not noted at all*) |
1853 those should not only be concealed but rather not noted at all*) |
1854 val maybe_conceal_notes = note_all = false ? map (apfst (apfst Binding.conceal)); |
1854 val maybe_conceal_notes = note_all = false ? map (apfst (apfst Binding.conceal)); |
1855 in |
1855 in |
1856 timer; |
1856 timer; |
1857 ({Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, xtor_co_folds = folds, |
1857 ({Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, xtor_co_recs = recs, |
1858 xtor_co_recs = recs, xtor_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms, |
1858 xtor_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms, |
1859 ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms, |
1859 ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms, |
1860 xtor_map_thms = ctor_Imap_thms, xtor_set_thmss = ctor_Iset_thmss', |
1860 xtor_map_thms = ctor_Imap_thms, xtor_set_thmss = ctor_Iset_thmss', |
1861 xtor_rel_thms = ctor_Irel_thms, xtor_co_fold_thms = ctor_fold_thms, |
1861 xtor_rel_thms = ctor_Irel_thms, xtor_co_rec_thms = ctor_rec_thms, |
1862 xtor_co_rec_thms = ctor_rec_thms, xtor_co_fold_o_map_thms = ctor_fold_o_Imap_thms, |
|
1863 xtor_co_rec_o_map_thms = ctor_rec_o_Imap_thms, rel_xtor_co_induct_thm = Irel_induct_thm}, |
1862 xtor_co_rec_o_map_thms = ctor_rec_o_Imap_thms, rel_xtor_co_induct_thm = Irel_induct_thm}, |
1864 lthy |> Local_Theory.notes (maybe_conceal_notes (common_notes @ notes @ Ibnf_notes)) |> snd) |
1863 lthy |> Local_Theory.notes (maybe_conceal_notes (common_notes @ notes @ Ibnf_notes)) |> snd) |
1865 end; |
1864 end; |
1866 |
1865 |
1867 val _ = |
1866 val _ = |