changeset 37744 | 3daaf23b9ab4 |
parent 37593 | 2505feaf2d70 |
child 38317 | cb8e2ac6397b |
37743:0a3fa8fbcdc5 | 37744:3daaf23b9ab4 |
---|---|
1 (* Title: HOL/Tools/Quotient/quotient_tacs.thy |
1 (* Title: HOL/Tools/Quotient/quotient_tacs.ML |
2 Author: Cezary Kaliszyk and Christian Urban |
2 Author: Cezary Kaliszyk and Christian Urban |
3 |
3 |
4 Tactics for solving goal arising from lifting theorems to quotient |
4 Tactics for solving goal arising from lifting theorems to quotient |
5 types. |
5 types. |
6 *) |
6 *) |