| changeset 16417 | 9bc16273c2d4 |
| parent 15140 | 322485b816ac |
| child 16836 | 45a3dc4688bc |
--- a/src/HOL/Presburger.thy Fri Jun 17 11:35:35 2005 +0200 +++ b/src/HOL/Presburger.thy Fri Jun 17 16:12:49 2005 +0200 @@ -10,7 +10,7 @@ theory Presburger imports NatSimprocs SetInterval -files ("cooper_dec.ML") ("cooper_proof.ML") ("qelim.ML") ("presburger.ML") +uses ("cooper_dec.ML") ("cooper_proof.ML") ("qelim.ML") ("presburger.ML") begin text {* Theorem for unitifying the coeffitients of @{text x} in an existential formula*}