changeset 37744 | 3daaf23b9ab4 |
parent 36603 | d5d6111761a6 |
child 38558 | 32ad17fe2b9c |
37743:0a3fa8fbcdc5 | 37744:3daaf23b9ab4 |
---|---|
1 (* Title: HOL/simpdata.ML |
1 (* Title: HOL/Tools/simpdata.ML |
2 Author: Tobias Nipkow |
2 Author: Tobias Nipkow |
3 Copyright 1991 University of Cambridge |
3 Copyright 1991 University of Cambridge |
4 |
4 |
5 Instantiation of the generic simplifier for HOL. |
5 Instantiation of the generic simplifier for HOL. |
6 *) |
6 *) |