src/HOL/Tools/inductive_package.ML
changeset 9893 93d2fde0306c
parent 9831 9b883c416aef
child 9939 44af7faa677e
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Thu Sep 07 20:50:33 2000 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Thu Sep 07 20:51:07 2000 +0200
     1.3 @@ -836,7 +836,7 @@
     1.4   [InductiveData.init,
     1.5    Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args,
     1.6      "dynamic case analysis on sets")],
     1.7 -  Attrib.add_attributes [("mono", mono_attr, "monotonicity rule")]];
     1.8 +  Attrib.add_attributes [("mono", mono_attr, "declaration of monotonicity rule")]];
     1.9  
    1.10  
    1.11  (* outer syntax *)