| changeset 37744 | 3daaf23b9ab4 |
| parent 36692 | 54b64d4ad524 |
| child 42361 | 23f352990944 |
| 37743:0a3fa8fbcdc5 | 37744:3daaf23b9ab4 |
|---|---|
1 (* |
1 (* Title: Provers/trancl.ML |
2 Title: Transitivity reasoner for transitive closures of relations |
|
3 Author: Oliver Kutter, TU Muenchen |
2 Author: Oliver Kutter, TU Muenchen |
3 |
|
4 Transitivity reasoner for transitive closures of relations |
|
4 *) |
5 *) |
5 |
6 |
6 (* |
7 (* |
7 |
8 |
8 The packages provides tactics trancl_tac and rtrancl_tac that prove |
9 The packages provides tactics trancl_tac and rtrancl_tac that prove |