src/HOL/Presburger.thy
changeset 30656 ddb1fafa2dcb
parent 30549 d2d7874648bd
child 30686 47a32dd1b86e
equal deleted inserted replaced
30655:88131f2807b6 30656:ddb1fafa2dcb
     5 header {* Decision Procedure for Presburger Arithmetic *}
     5 header {* Decision Procedure for Presburger Arithmetic *}
     6 
     6 
     7 theory Presburger
     7 theory Presburger
     8 imports Groebner_Basis SetInterval
     8 imports Groebner_Basis SetInterval
     9 uses
     9 uses
       
    10   "Tools/Qelim/qelim.ML"
    10   "Tools/Qelim/cooper_data.ML"
    11   "Tools/Qelim/cooper_data.ML"
    11   "Tools/Qelim/generated_cooper.ML"
    12   "Tools/Qelim/generated_cooper.ML"
    12   ("Tools/Qelim/cooper.ML")
    13   ("Tools/Qelim/cooper.ML")
    13   ("Tools/Qelim/presburger.ML")
    14   ("Tools/Qelim/presburger.ML")
    14 begin
    15 begin