src/HOL/Tools/Datatype/datatype_aux.ML
changeset 32712 ec5976f4d3d8
parent 32124 954321008785
child 32718 45929374f1bd
     1.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML	Fri Sep 25 10:20:03 2009 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Sun Sep 27 09:52:23 2009 +0200
     1.3 @@ -195,10 +195,11 @@
     1.4     rec_rewrites : thm list,
     1.5     case_name : string,
     1.6     case_rewrites : thm list,
     1.7 -   induction : thm,
     1.8 -   exhaustion : thm,
     1.9 +   inducts : thm list * thm,
    1.10 +   exhaust : thm,
    1.11     distinct : simproc_dist,
    1.12     inject : thm list,
    1.13 +   splits : thm * thm,
    1.14     nchotomy : thm,
    1.15     case_cong : thm,
    1.16     weak_case_cong : thm};