# HG changeset patch
# User wenzelm
# Date 1112858770 -7200
# Node ID 7e3bee7df06e036beace6ffdf0cd90b772af984f
# Parent  9ef583b0864742b2562f5a8c9c85c6b19960a82b
improved comments;

diff -r 9ef583b08647 -r 7e3bee7df06e src/Provers/hypsubst.ML
--- a/src/Provers/hypsubst.ML	Thu Apr 07 09:25:33 2005 +0200
+++ b/src/Provers/hypsubst.ML	Thu Apr 07 09:26:10 2005 +0200
@@ -3,7 +3,7 @@
     Authors:    Martin D Coen, Tobias Nipkow and Lawrence C Paulson
     Copyright   1995  University of Cambridge
 
-Basic equational reasoning: (hyp_)subst method and symmetric attribute.
+Basic equational reasoning: hyp_subst_tac and methods "hypsubst", "subst".
 
 Tactic to substitute using (at least) the assumption x=t in the rest
 of the subgoal, and to delete (at least) that assumption.  Original