src/HOL/Presburger.thy
changeset 23146 0bc590051d95
parent 22801 caffcb450ef4
child 23148 ef3fa1386102
     1.1 --- a/src/HOL/Presburger.thy	Thu May 31 11:00:06 2007 +0200
     1.2 +++ b/src/HOL/Presburger.thy	Thu May 31 12:06:31 2007 +0200
     1.3 @@ -9,10 +9,14 @@
     1.4  header {* Presburger Arithmetic: Cooper's Algorithm *}
     1.5  
     1.6  theory Presburger
     1.7 -imports NatSimprocs "../SetInterval"
     1.8 +imports "Integ/NatSimprocs" SetInterval
     1.9  uses
    1.10 -  ("cooper_dec.ML") ("cooper_proof.ML") ("qelim.ML") 
    1.11 -  ("reflected_presburger.ML") ("reflected_cooper.ML") ("presburger.ML")
    1.12 +  ("Tools/Presburger/cooper_dec.ML")
    1.13 +  ("Tools/Presburger/cooper_proof.ML")
    1.14 +  ("Tools/Presburger/qelim.ML") 
    1.15 +  ("Tools/Presburger/reflected_presburger.ML")
    1.16 +  ("Tools/Presburger/reflected_cooper.ML")
    1.17 +  ("Tools/Presburger/presburger.ML")
    1.18  begin
    1.19  
    1.20  text {* Theorem for unitifying the coeffitients of @{text x} in an existential formula*}
    1.21 @@ -1047,15 +1051,15 @@
    1.22    show ?thesis by (simp add: 1)
    1.23  qed
    1.24  
    1.25 -use "cooper_dec.ML"
    1.26 -use "reflected_presburger.ML" 
    1.27 -use "reflected_cooper.ML"
    1.28 +use "Tools/Presburger/cooper_dec.ML"
    1.29 +use "Tools/Presburger/reflected_presburger.ML" 
    1.30 +use "Tools/Presburger/reflected_cooper.ML"
    1.31  oracle
    1.32    presburger_oracle ("term") = ReflectedCooper.presburger_oracle
    1.33  
    1.34 -use "cooper_proof.ML"
    1.35 -use "qelim.ML"
    1.36 -use "presburger.ML"
    1.37 +use "Tools/Presburger/cooper_proof.ML"
    1.38 +use "Tools/Presburger/qelim.ML"
    1.39 +use "Tools/Presburger/presburger.ML"
    1.40  
    1.41  setup "Presburger.setup"
    1.42