--- a/src/HOL/Tools/sat.ML Sun Nov 26 13:19:52 2017 +0100
+++ b/src/HOL/Tools/sat.ML Sun Nov 26 21:08:32 2017 +0100
@@ -71,7 +71,7 @@
val counter = Unsynchronized.ref 0;
val resolution_thm =
- @{lemma "(P ==> False) ==> (~ P ==> False) ==> False" by (rule case_split)}
+ @{lemma "(P \<Longrightarrow> False) \<Longrightarrow> (\<not> P \<Longrightarrow> False) \<Longrightarrow> False" by (rule case_split)}
(* ------------------------------------------------------------------------- *)
(* lit_ord: an order on integers that considers their absolute values only, *)