changeset 14981 | e73f8140af78 |
parent 14941 | 1edb674e0c33 |
child 15013 | 34264f5e4691 |
--- a/src/HOL/Presburger.thy Sun Jun 20 09:30:12 2004 +0200 +++ b/src/HOL/Presburger.thy Mon Jun 21 10:25:57 2004 +0200 @@ -1,7 +1,6 @@ (* Title: HOL/Integ/Presburger.thy ID: $Id$ Author: Amine Chaieb, Tobias Nipkow and Stefan Berghofer, TU Muenchen - License: GPL (GNU GENERAL PUBLIC LICENSE) File containing necessary theorems for the proof generation for Cooper Algorithm