src/Provers/hypsubst.ML
changeset 15662 7e3bee7df06e
parent 15531 08c8dad8e399
child 16979 4d4d42ea3096
--- 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