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.
no computation rules in the pre-simplifiaction set
authorchaieb
Thu, 14 Jun 2007 22:59:40 +0200
changeset 23391 a7c128816edc
parent 23390 01ef1135de73
child 23392 4b03e3586f7f
no computation rules in the pre-simplifiaction set
src/HOL/Tools/Presburger/cooper_data.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Presburger/cooper_data.ML	Thu Jun 14 22:59:39 2007 +0200
+++ b/src/HOL/Tools/Presburger/cooper_data.ML	Thu Jun 14 22:59:40 2007 +0200
@@ -16,8 +16,8 @@
 struct
 
 type entry = simpset* (term list);
-val start_ss = HOL_ss addsimps @{thms "Groebner_Basis.comp_arith"}
-               addcongs [if_weak_cong, @{thm "let_weak_cong"}];
+val start_ss = HOL_ss (* addsimps @{thms "Groebner_Basis.comp_arith"}
+               addcongs [if_weak_cong, @{thm "let_weak_cong"}];*)
 val allowed_consts = 
   [@{term "op + :: int => _"}, @{term "op + :: nat => _"}, 
    @{term "op - :: int => _"}, @{term "op - :: nat => _"},
isabelle