src/HOL/Tools/Datatype/datatype_data.ML
changeset 56858 0c3d0bc98abe
parent 56375 32e0da92c786
child 57983 6edc3529bb4e
equal deleted inserted replaced
56857:aa2de99be748 56858:0c3d0bc98abe
   107    case_thms = case_rewrites,
   107    case_thms = case_rewrites,
   108    case_cong = case_cong,
   108    case_cong = case_cong,
   109    weak_case_cong = weak_case_cong,
   109    weak_case_cong = weak_case_cong,
   110    split = split,
   110    split = split,
   111    split_asm = split_asm,
   111    split_asm = split_asm,
       
   112    disc_defs = [],
   112    disc_thmss = [],
   113    disc_thmss = [],
   113    discIs = [],
   114    discIs = [],
       
   115    sel_defs = [],
   114    sel_thmss = [],
   116    sel_thmss = [],
   115    disc_excludesss = [],
   117    disc_excludesss = [],
   116    disc_exhausts = [],
   118    disc_exhausts = [],
   117    sel_exhausts = [],
   119    sel_exhausts = [],
   118    collapses = [],
   120    collapses = [],