| changeset 23148 | ef3fa1386102 |
| parent 22997 | d4f3b015b50b |
| child 23253 | b1f3f53c60b5 |
| 23147:a5db2f7d7654 | 23148:ef3fa1386102 |
|---|---|
1 (* Title: HOL/Integ/cooper_dec.ML |
1 (* Title: HOL/Tools/Presburger/cooper_dec.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Amine Chaieb and Tobias Nipkow, TU Muenchen |
3 Author: Amine Chaieb and Tobias Nipkow, TU Muenchen |
4 |
4 |
5 File containing the implementation of Cooper Algorithm |
5 File containing the implementation of Cooper Algorithm |
6 decision procedure (intensively inspired from J.Harrison) |
6 decision procedure (intensively inspired from J.Harrison) |