Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Presburger.thy
changeset 63962 83a625d06e91
parent 63961 2fd9656c4c82
child 64242 93c6f0da5c70
equal deleted inserted replaced
63961:2fd9656c4c82 63962:83a625d06e91 
     3 *)
 
     3 *)
 
     4 
     4 
     5 section \<open>Decision Procedure for Presburger Arithmetic\<close>
 
     5 section \<open>Decision Procedure for Presburger Arithmetic\<close>
 
     6 
     6 
     7 theory Presburger
 
     7 theory Presburger
 
     8 imports Groebner_Basis Set_Interval Argo
 
     8 imports Groebner_Basis Set_Interval
 
     9 keywords "try0" :: diag
 
     9 keywords "try0" :: diag
 
    10 begin
 
    10 begin
 
    11 
    11 
    12 ML_file "Tools/Qelim/qelim.ML"
 
    12 ML_file "Tools/Qelim/qelim.ML"
 
    13 ML_file "Tools/Qelim/cooper_procedure.ML"
 
    13 ML_file "Tools/Qelim/cooper_procedure.ML"
isabelle