improved comments;
authorwenzelm
Thu Apr 07 09:26:10 2005 +0200 (2005-04-07 ago)
changeset 156627e3bee7df06e
parent 15661 9ef583b08647
child 15663 6e6233e8cf5e
improved comments;
src/Provers/hypsubst.ML
     1.1 --- a/src/Provers/hypsubst.ML	Thu Apr 07 09:25:33 2005 +0200
     1.2 +++ b/src/Provers/hypsubst.ML	Thu Apr 07 09:26:10 2005 +0200
     1.3 @@ -3,7 +3,7 @@
     1.4      Authors:    Martin D Coen, Tobias Nipkow and Lawrence C Paulson
     1.5      Copyright   1995  University of Cambridge
     1.6  
     1.7 -Basic equational reasoning: (hyp_)subst method and symmetric attribute.
     1.8 +Basic equational reasoning: hyp_subst_tac and methods "hypsubst", "subst".
     1.9  
    1.10  Tactic to substitute using (at least) the assumption x=t in the rest
    1.11  of the subgoal, and to delete (at least) that assumption.  Original