src/Provers/hypsubst.ML
changeset 9893 93d2fde0306c
parent 9705 8eecca293907
child 10821 dcb75538f542
--- 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;