src/Provers/hypsubst.ML

--- 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;