src/HOL/arith_data.ML
changeset 9893 93d2fde0306c
parent 9593 b732997cfc11
child 10516 dc113303d101
     1.1 --- a/src/HOL/arith_data.ML	Thu Sep 07 20:50:33 2000 +0200
     1.2 +++ b/src/HOL/arith_data.ML	Thu Sep 07 20:51:07 2000 +0200
     1.3 @@ -426,4 +426,4 @@
     1.4      "decide linear arithmethic")],
     1.5    Attrib.add_attributes [("arith_split",
     1.6      (Attrib.no_args arith_split_add, Attrib.no_args Attrib.undef_local_attribute),
     1.7 -    "declare split rules for arithmetic procedure")]];
     1.8 +    "declaration of split rules for arithmetic procedure")]];