src/HOL/Presburger.thy
changeset 48891 c0eafbd55de3
parent 47432 e1576d13e933
child 49962 a8cc904a6820
     1.1 --- a/src/HOL/Presburger.thy	Wed Aug 22 22:47:16 2012 +0200
     1.2 +++ b/src/HOL/Presburger.thy	Wed Aug 22 22:55:41 2012 +0200
     1.3 @@ -6,12 +6,11 @@
     1.4  
     1.5  theory Presburger
     1.6  imports Groebner_Basis Set_Interval
     1.7 -uses
     1.8 -  "Tools/Qelim/qelim.ML"
     1.9 -  "Tools/Qelim/cooper_procedure.ML"
    1.10 -  ("Tools/Qelim/cooper.ML")
    1.11  begin
    1.12  
    1.13 +ML_file "Tools/Qelim/qelim.ML"
    1.14 +ML_file "Tools/Qelim/cooper_procedure.ML"
    1.15 +
    1.16  subsection{* The @{text "-\<infinity>"} and @{text "+\<infinity>"} Properties *}
    1.17  
    1.18  lemma minf:
    1.19 @@ -386,7 +385,7 @@
    1.20    "\<lbrakk>x = x'; 0 \<le> x' \<Longrightarrow> P = P'\<rbrakk> \<Longrightarrow> (0 \<le> (x::int) \<and> P) = (0 \<le> x' \<and> P')"
    1.21    by (simp cong: conj_cong)
    1.22  
    1.23 -use "Tools/Qelim/cooper.ML"
    1.24 +ML_file "Tools/Qelim/cooper.ML"
    1.25  setup Cooper.setup
    1.26  
    1.27  method_setup presburger = {*