equal
deleted
inserted
replaced
1 (* Title: HOL/Integ/presburger.ML |
1 (* Title: HOL/Integ/presburger.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Amine Chaieb and Stefan Berghofer, TU Muenchen |
3 Author: Amine Chaieb and Stefan Berghofer, TU Muenchen |
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
5 |
4 |
6 Tactic for solving arithmetical Goals in Presburger Arithmetic |
5 Tactic for solving arithmetical Goals in Presburger Arithmetic |
7 *) |
6 *) |
8 |
7 |
9 (* This version of presburger deals with occurences of functional symbols in the subgoal and abstract over them to try to prove the more general formula. It then resolves with the subgoal. To enable this feature call the procedure with the parameter abs |
8 (* This version of presburger deals with occurences of functional symbols in the subgoal and abstract over them to try to prove the more general formula. It then resolves with the subgoal. To enable this feature call the procedure with the parameter abs |