--- a/src/HOL/Integ/Presburger.thy Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Integ/Presburger.thy Mon Aug 16 14:22:27 2004 +0200
@@ -6,14 +6,12 @@
generation for Cooper Algorithm
*)
-header {* Presburger Arithmetic: Cooper Algorithm *}
+header {* Presburger Arithmetic: Cooper's Algorithm *}
-theory Presburger = NatSimprocs + SetInterval
-files
- ("cooper_dec.ML")
- ("cooper_proof.ML")
- ("qelim.ML")
- ("presburger.ML"):
+theory Presburger
+import NatSimprocs SetInterval
+files ("cooper_dec.ML") ("cooper_proof.ML") ("qelim.ML") ("presburger.ML")
+begin
text {* Theorem for unitifying the coeffitients of @{text x} in an existential formula*}