tuned msg;
authorwenzelm
Thu Sep 07 20:51:07 2000 +0200 (2000-09-07)
changeset 989393d2fde0306c
parent 9892 be0389a64ce8
child 9894 c8ff37b637a7
tuned msg;
src/HOL/Tools/induct_method.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/recdef_package.ML
src/HOL/arith_data.ML
src/Provers/clasimp.ML
src/Provers/hypsubst.ML
     1.1 --- a/src/HOL/Tools/induct_method.ML	Thu Sep 07 20:50:33 2000 +0200
     1.2 +++ b/src/HOL/Tools/induct_method.ML	Thu Sep 07 20:51:07 2000 +0200
     1.3 @@ -453,8 +453,8 @@
     1.4  val setup =
     1.5    [GlobalInduct.init, LocalInduct.init,
     1.6     Attrib.add_attributes
     1.7 -    [(casesN, cases_attr, "cases rule for type or set"),
     1.8 -     (inductN, induct_attr, "induction rule for type or set")],
     1.9 +    [(casesN, cases_attr, "declaration of cases rule for type or set"),
    1.10 +     (inductN, induct_attr, "declaration of induction rule for type or set")],
    1.11     Method.add_methods
    1.12      [("cases", cases_meth oo cases_args, "case analysis on types or sets"),
    1.13       ("induct", induct_meth oo induct_args, "induction on types or sets")],
     2.1 --- a/src/HOL/Tools/inductive_package.ML	Thu Sep 07 20:50:33 2000 +0200
     2.2 +++ b/src/HOL/Tools/inductive_package.ML	Thu Sep 07 20:51:07 2000 +0200
     2.3 @@ -836,7 +836,7 @@
     2.4   [InductiveData.init,
     2.5    Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args,
     2.6      "dynamic case analysis on sets")],
     2.7 -  Attrib.add_attributes [("mono", mono_attr, "monotonicity rule")]];
     2.8 +  Attrib.add_attributes [("mono", mono_attr, "declaration of monotonicity rule")]];
     2.9  
    2.10  
    2.11  (* outer syntax *)
     3.1 --- a/src/HOL/Tools/recdef_package.ML	Thu Sep 07 20:50:33 2000 +0200
     3.2 +++ b/src/HOL/Tools/recdef_package.ML	Thu Sep 07 20:51:07 2000 +0200
     3.3 @@ -305,9 +305,9 @@
     3.4  val setup =
     3.5   [GlobalRecdefData.init, LocalRecdefData.init,
     3.6    Attrib.add_attributes
     3.7 -   [("recdef_simp", simp_attr, "declare recdef simp rule"),
     3.8 -    ("recdef_cong", cong_attr, "declare recdef cong rule"),
     3.9 -    ("recdef_wf", wf_attr, "declare recdef wf rule")]];
    3.10 +   [("recdef_simp", simp_attr, "declaration of recdef simp rule"),
    3.11 +    ("recdef_cong", cong_attr, "declaration of recdef cong rule"),
    3.12 +    ("recdef_wf", wf_attr, "declaration of recdef wf rule")]];
    3.13  
    3.14  
    3.15  (* outer syntax *)
     4.1 --- a/src/HOL/arith_data.ML	Thu Sep 07 20:50:33 2000 +0200
     4.2 +++ b/src/HOL/arith_data.ML	Thu Sep 07 20:51:07 2000 +0200
     4.3 @@ -426,4 +426,4 @@
     4.4      "decide linear arithmethic")],
     4.5    Attrib.add_attributes [("arith_split",
     4.6      (Attrib.no_args arith_split_add, Attrib.no_args Attrib.undef_local_attribute),
     4.7 -    "declare split rules for arithmetic procedure")]];
     4.8 +    "declaration of split rules for arithmetic procedure")]];
     5.1 --- a/src/Provers/clasimp.ML	Thu Sep 07 20:50:33 2000 +0200
     5.2 +++ b/src/Provers/clasimp.ML	Thu Sep 07 20:51:07 2000 +0200
     5.3 @@ -308,7 +308,7 @@
     5.4  
     5.5  val setup =
     5.6   [Attrib.add_attributes
     5.7 -  [("iff", iff_attr, "declare simplifier / classical rules")],
     5.8 +  [("iff", iff_attr, "declaration of Simplifier / Classical rules")],
     5.9    Method.add_methods
    5.10     [("fastsimp", clasimp_method' fast_simp_tac, "combined fast and simp"),
    5.11      ("slowsimp", clasimp_method' slow_simp_tac, "combined slow and simp"),
     6.1 --- a/src/Provers/hypsubst.ML	Thu Sep 07 20:50:33 2000 +0200
     6.2 +++ b/src/Provers/hypsubst.ML	Thu Sep 07 20:51:07 2000 +0200
     6.3 @@ -276,6 +276,6 @@
     6.4    [("hypsubst", hyp_subst_meth, "substitution using an assumption (improper)"),
     6.5     ("subst", subst_meth, "substitution")],
     6.6    Attrib.add_attributes
     6.7 -  [("symmetric", (gen_symmetric, gen_symmetric), "apply symmetry of == or =")]];
     6.8 +  [("symmetric", (gen_symmetric, gen_symmetric), "resolution with symmetry of == or =")]];
     6.9  
    6.10  end;