Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned relevance test for presburger
authorchaieb
Thu, 03 Jan 2008 18:19:27 +0100
changeset 25811 f7c048eafa90
parent 25810 bac99880fa99
child 25812 687ee352c891
tuned relevance test for presburger
src/HOL/Tools/Qelim/presburger.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Qelim/presburger.ML	Thu Jan 03 17:50:44 2008 +0100
+++ b/src/HOL/Tools/Qelim/presburger.ML	Thu Jan 03 18:19:27 2008 +0100
@@ -85,9 +85,9 @@
  in h [] end;
 in 
 fun is_relevant ctxt ct = 
-  gen_subset (op aconv) (term_constants (term_of ct) , snd (CooperData.get ctxt))
- andalso forall (fn Free (_,T) => T = HOLogic.intT) (term_frees (term_of ct))
- andalso forall (fn Var (_,T) => T = HOLogic.intT) (term_vars (term_of ct));
+ gen_subset (op aconv) (term_constants (term_of ct) , snd (CooperData.get ctxt))
+ andalso forall (fn Free (_,T) => T mem [@{typ "int"}, @{typ nat}]) (term_frees (term_of ct))
+ andalso forall (fn Var (_,T) => T mem [@{typ "int"}, @{typ nat}]) (term_vars (term_of ct));
 
 fun int_nat_terms ctxt ct =
  let
isabelle