src/HOL/Integ/Presburger.thy
changeset 17378 105519771c67
parent 16836 45a3dc4688bc
child 17589 58eeffd73be1
     1.1 --- a/src/HOL/Integ/Presburger.thy	Wed Sep 14 10:24:39 2005 +0200
     1.2 +++ b/src/HOL/Integ/Presburger.thy	Wed Sep 14 17:25:52 2005 +0200
     1.3 @@ -10,7 +10,8 @@
     1.4  
     1.5  theory Presburger
     1.6  imports NatSimprocs SetInterval
     1.7 -uses ("cooper_dec.ML") ("cooper_proof.ML") ("qelim.ML") ("presburger.ML")
     1.8 +uses ("cooper_dec.ML") ("cooper_proof.ML") ("qelim.ML") 
     1.9 +	("reflected_presburger.ML") ("reflected_cooper.ML") ("presburger.ML")
    1.10  begin
    1.11  
    1.12  text {* Theorem for unitifying the coeffitients of @{text x} in an existential formula*}
    1.13 @@ -982,8 +983,10 @@
    1.14    by (simp cong: conj_cong)
    1.15  
    1.16  use "cooper_dec.ML"
    1.17 +use "reflected_presburger.ML" 
    1.18 +use "reflected_cooper.ML"
    1.19  oracle
    1.20 -  presburger_oracle ("term") = CooperDec.presburger_oracle
    1.21 +  presburger_oracle ("term") = ReflectedCooper.presburger_oracle
    1.22  
    1.23  use "cooper_proof.ML"
    1.24  use "qelim.ML"