equal
deleted
inserted
replaced
1 (* Title: Provers/hypsubst.ML |
1 (* Title: Provers/hypsubst.ML |
2 Authors: Martin D Coen, Tobias Nipkow and Lawrence C Paulson |
2 Authors: Martin D Coen, Tobias Nipkow and Lawrence C Paulson |
3 Copyright 1995 University of Cambridge |
3 Copyright 1995 University of Cambridge |
4 |
4 |
5 Basic equational reasoning: hyp_subst_tac and methods "hypsubst", "subst". |
5 Basic equational reasoning: hyp_subst_tac and methods "hypsubst", "simplesubst". |
6 |
6 |
7 Tactic to substitute using (at least) the assumption x=t in the rest |
7 Tactic to substitute using (at least) the assumption x=t in the rest |
8 of the subgoal, and to delete (at least) that assumption. Original |
8 of the subgoal, and to delete (at least) that assumption. Original |
9 version due to Martin Coen. |
9 version due to Martin Coen. |
10 |
10 |