src/HOL/Tools/Presburger/cooper_data.ML
changeset 23391 a7c128816edc
parent 23336 21a7433c4bd3
child 23461 9a586e80ce15
equal deleted inserted replaced
23390:01ef1135de73 23391:a7c128816edc
    14 
    14 
    15 structure Cooper_Data : COOPER_DATA =
    15 structure Cooper_Data : COOPER_DATA =
    16 struct
    16 struct
    17 
    17 
    18 type entry = simpset* (term list);
    18 type entry = simpset* (term list);
    19 val start_ss = HOL_ss addsimps @{thms "Groebner_Basis.comp_arith"}
    19 val start_ss = HOL_ss (* addsimps @{thms "Groebner_Basis.comp_arith"}
    20                addcongs [if_weak_cong, @{thm "let_weak_cong"}];
    20                addcongs [if_weak_cong, @{thm "let_weak_cong"}];*)
    21 val allowed_consts = 
    21 val allowed_consts = 
    22   [@{term "op + :: int => _"}, @{term "op + :: nat => _"}, 
    22   [@{term "op + :: int => _"}, @{term "op + :: nat => _"}, 
    23    @{term "op - :: int => _"}, @{term "op - :: nat => _"}, 
    23    @{term "op - :: int => _"}, @{term "op - :: nat => _"}, 
    24    @{term "op * :: int => _"}, @{term "op * :: nat => _"}, 
    24    @{term "op * :: int => _"}, @{term "op * :: nat => _"}, 
    25    @{term "op div :: int => _"}, @{term "op div :: nat => _"}, 
    25    @{term "op div :: int => _"}, @{term "op div :: nat => _"},