changeset 56851 | 35ff4ede3409 |
parent 56846 | 9df717fef2bb |
child 56853 | a265e41cc33b |
--- a/src/HOL/Library/refute.ML Sun May 04 18:53:58 2014 +0200 +++ b/src/HOL/Library/refute.ML Sun May 04 18:57:45 2014 +0200 @@ -1068,7 +1068,7 @@ val fm_ax = Prop_Logic.all (map toTrue (tl intrs)) val fm = Prop_Logic.all [#wellformed args, fm_ax, fm_u] val _ = - (if member (op =) ["dpll_p"] satsolver then + (if member (op =) ["cdclite"] satsolver then warning ("Using SAT solver " ^ quote satsolver ^ "; for better performance, consider installing an \ \external solver.")