# HG changeset patch
# User blanchet
# Date 1288122230 -7200
# Node ID 8819ffd603576b7a8e18c2b65e47cc9a32094a0b
# Parent  277508b0741802f7ed15e371c433de1237822791
better list of irrelevant SMT constants

diff -r 277508b07418 -r 8819ffd60357 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Oct 26 21:34:01 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Oct 26 21:43:50 2010 +0200
@@ -115,7 +115,27 @@
 val atp_irrelevant_consts =
   [@{const_name False}, @{const_name True}, @{const_name If}, @{const_name Let},
    @{const_name HOL.eq}]
-val smt_irrelevant_consts = atp_irrelevant_consts (* FIXME *)
+
+(* FIXME: check types *)
+val smt_irrelevant_consts =
+  atp_irrelevant_consts @
+  [@{const_name distinct},
+   (* numeral-related: *)
+   @{const_name number_of}, @{const_name Int.Pls}, @{const_name Int.Min},
+   @{const_name Int.Bit0}, @{const_name Int.Bit1}, @{const_name Suc},
+   (* FIXME: @{const_name Numeral0}, @{const_name Numeral1}, *)
+   (* int => nat *)
+   @{const_name nat},
+   (* nat => int *)
+   (* FIXME: @{const_name int}, *)
+   (* for "nat", "int", and "real": *)
+   @{const_name plus}, @{const_name uminus}, @{const_name minus},
+   @{const_name times}, @{const_name less}, @{const_name less_eq},
+   @{const_name abs}, @{const_name min}, @{const_name max},
+   (* for "nat" and "div": *)
+   @{const_name div}, @{const_name mod} (* , *)
+   (* for real: *)
+   (* FIXME: @{const_name "op /"} *)]
 
 fun irrelevant_consts_for_prover name =
   if is_smt_prover name then smt_irrelevant_consts else atp_irrelevant_consts