diff -r 5d8faadf3ecf -r 0bc590051d95 src/HOL/Presburger.thy --- a/src/HOL/Presburger.thy Thu May 31 11:00:06 2007 +0200 +++ b/src/HOL/Presburger.thy Thu May 31 12:06:31 2007 +0200 @@ -9,10 +9,14 @@ header {* Presburger Arithmetic: Cooper's Algorithm *} theory Presburger -imports NatSimprocs "../SetInterval" +imports "Integ/NatSimprocs" SetInterval uses - ("cooper_dec.ML") ("cooper_proof.ML") ("qelim.ML") - ("reflected_presburger.ML") ("reflected_cooper.ML") ("presburger.ML") + ("Tools/Presburger/cooper_dec.ML") + ("Tools/Presburger/cooper_proof.ML") + ("Tools/Presburger/qelim.ML") + ("Tools/Presburger/reflected_presburger.ML") + ("Tools/Presburger/reflected_cooper.ML") + ("Tools/Presburger/presburger.ML") begin text {* Theorem for unitifying the coeffitients of @{text x} in an existential formula*} @@ -1047,15 +1051,15 @@ show ?thesis by (simp add: 1) qed -use "cooper_dec.ML" -use "reflected_presburger.ML" -use "reflected_cooper.ML" +use "Tools/Presburger/cooper_dec.ML" +use "Tools/Presburger/reflected_presburger.ML" +use "Tools/Presburger/reflected_cooper.ML" oracle presburger_oracle ("term") = ReflectedCooper.presburger_oracle -use "cooper_proof.ML" -use "qelim.ML" -use "presburger.ML" +use "Tools/Presburger/cooper_proof.ML" +use "Tools/Presburger/qelim.ML" +use "Tools/Presburger/presburger.ML" setup "Presburger.setup"