# HG changeset patch
# User chaieb
# Date 1181854780 -7200
# Node ID a7c128816edc853a372ed1d3f46e675434b0dd8a
# Parent  01ef1135de7333bcea3977548bac72211b8660cf
no computation rules in the pre-simplifiaction set

diff -r 01ef1135de73 -r a7c128816edc src/HOL/Tools/Presburger/cooper_data.ML
--- 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 => _"},