tuned;
authorwenzelm
Sat Jul 08 12:54:39 2006 +0200 (2006-07-08)
changeset 20051859e7129961b
parent 20050 a2fb9d553aad
child 20052 3d4ff822d0b3
tuned;
src/HOL/Integ/Presburger.thy
src/HOL/Presburger.thy
     1.1 --- a/src/HOL/Integ/Presburger.thy	Sat Jul 08 12:54:38 2006 +0200
     1.2 +++ b/src/HOL/Integ/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
     2.1 --- a/src/HOL/Presburger.thy	Sat Jul 08 12:54:38 2006 +0200
     2.2 +++ b/src/HOL/Presburger.thy	Sat Jul 08 12:54:39 2006 +0200
     2.3 @@ -9,7 +9,7 @@
     2.4  header {* Presburger Arithmetic: Cooper's Algorithm *}
     2.5  
     2.6  theory Presburger
     2.7 -imports NatSimprocs SetInterval
     2.8 +imports NatSimprocs
     2.9  uses ("cooper_dec.ML") ("cooper_proof.ML") ("qelim.ML") 
    2.10  	("reflected_presburger.ML") ("reflected_cooper.ML") ("presburger.ML")
    2.11  begin