src/HOL/Presburger.thy
changeset 20051 859e7129961b
parent 18202 46af82efd311
child 20217 25b068a99d2b
     1.1 --- a/src/HOL/Presburger.thy	Sat Jul 08 12:54:38 2006 +0200
     1.2 +++ b/src/HOL/Presburger.thy	Sat Jul 08 12:54:39 2006 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  header {* Presburger Arithmetic: Cooper's Algorithm *}
     1.5  
     1.6  theory Presburger
     1.7 -imports NatSimprocs SetInterval
     1.8 +imports NatSimprocs
     1.9  uses ("cooper_dec.ML") ("cooper_proof.ML") ("qelim.ML") 
    1.10  	("reflected_presburger.ML") ("reflected_cooper.ML") ("presburger.ML")
    1.11  begin