src/HOL/Integ/Presburger.thy
changeset 15131 c69542757a4d
parent 15013 34264f5e4691
child 15140 322485b816ac
     1.1 --- a/src/HOL/Integ/Presburger.thy	Mon Aug 16 14:21:54 2004 +0200
     1.2 +++ b/src/HOL/Integ/Presburger.thy	Mon Aug 16 14:22:27 2004 +0200
     1.3 @@ -6,14 +6,12 @@
     1.4  generation for Cooper Algorithm  
     1.5  *)
     1.6  
     1.7 -header {* Presburger Arithmetic: Cooper Algorithm *}
     1.8 +header {* Presburger Arithmetic: Cooper's Algorithm *}
     1.9  
    1.10 -theory Presburger = NatSimprocs + SetInterval
    1.11 -files
    1.12 -  ("cooper_dec.ML")
    1.13 -  ("cooper_proof.ML")
    1.14 -  ("qelim.ML")
    1.15 -  ("presburger.ML"):
    1.16 +theory Presburger
    1.17 +import NatSimprocs SetInterval
    1.18 +files ("cooper_dec.ML") ("cooper_proof.ML") ("qelim.ML") ("presburger.ML")
    1.19 +begin
    1.20  
    1.21  text {* Theorem for unitifying the coeffitients of @{text x} in an existential formula*}
    1.22