src/HOL/Integ/Presburger.thy
changeset 14485 ea2707645af8
parent 14378 69c4d5997669
child 14577 dbb95b825244
     1.1 --- a/src/HOL/Integ/Presburger.thy	Thu Mar 25 10:31:25 2004 +0100
     1.2 +++ b/src/HOL/Integ/Presburger.thy	Thu Mar 25 10:32:21 2004 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  generation for Cooper Algorithm  
     1.5  *)
     1.6  
     1.7 -theory Presburger = NatSimprocs
     1.8 +theory Presburger = NatSimprocs + SetInterval
     1.9  files
    1.10    ("cooper_dec.ML")
    1.11    ("cooper_proof.ML")