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
```