src/HOL/Tools/datatype_aux.ML
changeset 10120 0f315aeee16e
parent 9740 1c5b0f27de56
child 11539 0f17da240450
     1.1 --- a/src/HOL/Tools/datatype_aux.ML	Mon Oct 02 12:35:48 2000 +0200
     1.2 +++ b/src/HOL/Tools/datatype_aux.ML	Mon Oct 02 14:21:12 2000 +0200
     1.3 @@ -173,7 +173,8 @@
     1.4     distinct : simproc_dist,
     1.5     inject : thm list,
     1.6     nchotomy : thm,
     1.7 -   case_cong : thm};
     1.8 +   case_cong : thm,
     1.9 +   weak_case_cong : thm};
    1.10  
    1.11  fun mk_Free s T i = Free (s ^ (string_of_int i), T);
    1.12