src/HOL/Tools/datatype_aux.ML
changeset 18319 c52b139ebde0
parent 18314 4595eb4627fa
child 18349 58de95a16d3c
equal deleted inserted replaced
18318:deb87d7e44bc 18319:c52b139ebde0
   181 type descr = (int * (string * dtyp list * (string * dtyp list) list)) list;
   181 type descr = (int * (string * dtyp list * (string * dtyp list) list)) list;
   182 
   182 
   183 type datatype_info =
   183 type datatype_info =
   184   {index : int,
   184   {index : int,
   185    descr : descr,
   185    descr : descr,
       
   186    sorts : (string * sort) list,
   186    rec_names : string list,
   187    rec_names : string list,
   187    rec_rewrites : thm list,
   188    rec_rewrites : thm list,
   188    case_name : string,
   189    case_name : string,
   189    case_rewrites : thm list,
   190    case_rewrites : thm list,
   190    induction : thm,
   191    induction : thm,