Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned msg;
authorwenzelm
Thu, 07 Sep 2000 20:51:07 +0200
changeset 9893 93d2fde0306c
parent 9892 be0389a64ce8
child 9894 c8ff37b637a7
tuned msg;
src/HOL/Tools/induct_method.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/inductive_package.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/recdef_package.ML file | annotate | diff | comparison | revisions
src/HOL/arith_data.ML file | annotate | diff | comparison | revisions
src/Provers/clasimp.ML file | annotate | diff | comparison | revisions
src/Provers/hypsubst.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/induct_method.ML	Thu Sep 07 20:50:33 2000 +0200
+++ b/src/HOL/Tools/induct_method.ML	Thu Sep 07 20:51:07 2000 +0200
@@ -453,8 +453,8 @@
 val setup =
   [GlobalInduct.init, LocalInduct.init,
    Attrib.add_attributes
-    [(casesN, cases_attr, "cases rule for type or set"),
-     (inductN, induct_attr, "induction rule for type or set")],
+    [(casesN, cases_attr, "declaration of cases rule for type or set"),
+     (inductN, induct_attr, "declaration of induction rule for type or set")],
    Method.add_methods
     [("cases", cases_meth oo cases_args, "case analysis on types or sets"),
      ("induct", induct_meth oo induct_args, "induction on types or sets")],
--- a/src/HOL/Tools/inductive_package.ML	Thu Sep 07 20:50:33 2000 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Thu Sep 07 20:51:07 2000 +0200
@@ -836,7 +836,7 @@
  [InductiveData.init,
   Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args,
     "dynamic case analysis on sets")],
-  Attrib.add_attributes [("mono", mono_attr, "monotonicity rule")]];
+  Attrib.add_attributes [("mono", mono_attr, "declaration of monotonicity rule")]];
 
 
 (* outer syntax *)
--- a/src/HOL/Tools/recdef_package.ML	Thu Sep 07 20:50:33 2000 +0200
+++ b/src/HOL/Tools/recdef_package.ML	Thu Sep 07 20:51:07 2000 +0200
@@ -305,9 +305,9 @@
 val setup =
  [GlobalRecdefData.init, LocalRecdefData.init,
   Attrib.add_attributes
-   [("recdef_simp", simp_attr, "declare recdef simp rule"),
-    ("recdef_cong", cong_attr, "declare recdef cong rule"),
-    ("recdef_wf", wf_attr, "declare recdef wf rule")]];
+   [("recdef_simp", simp_attr, "declaration of recdef simp rule"),
+    ("recdef_cong", cong_attr, "declaration of recdef cong rule"),
+    ("recdef_wf", wf_attr, "declaration of recdef wf rule")]];
 
 
 (* outer syntax *)
--- a/src/HOL/arith_data.ML	Thu Sep 07 20:50:33 2000 +0200
+++ b/src/HOL/arith_data.ML	Thu Sep 07 20:51:07 2000 +0200
@@ -426,4 +426,4 @@
     "decide linear arithmethic")],
   Attrib.add_attributes [("arith_split",
     (Attrib.no_args arith_split_add, Attrib.no_args Attrib.undef_local_attribute),
-    "declare split rules for arithmetic procedure")]];
+    "declaration of split rules for arithmetic procedure")]];
--- a/src/Provers/clasimp.ML	Thu Sep 07 20:50:33 2000 +0200
+++ b/src/Provers/clasimp.ML	Thu Sep 07 20:51:07 2000 +0200
@@ -308,7 +308,7 @@
 
 val setup =
  [Attrib.add_attributes
-  [("iff", iff_attr, "declare simplifier / classical rules")],
+  [("iff", iff_attr, "declaration of Simplifier / Classical rules")],
   Method.add_methods
    [("fastsimp", clasimp_method' fast_simp_tac, "combined fast and simp"),
     ("slowsimp", clasimp_method' slow_simp_tac, "combined slow and simp"),
--- a/src/Provers/hypsubst.ML	Thu Sep 07 20:50:33 2000 +0200
+++ b/src/Provers/hypsubst.ML	Thu Sep 07 20:51:07 2000 +0200
@@ -276,6 +276,6 @@
   [("hypsubst", hyp_subst_meth, "substitution using an assumption (improper)"),
    ("subst", subst_meth, "substitution")],
   Attrib.add_attributes
-  [("symmetric", (gen_symmetric, gen_symmetric), "apply symmetry of == or =")]];
+  [("symmetric", (gen_symmetric, gen_symmetric), "resolution with symmetry of == or =")]];
 
 end;
isabelle