# HG changeset patch
# User nipkow
# Date 1497706879 -7200
# Node ID e034a563ed7db5ad773f715600f76d46505e1e98
# Parent  8ff7fd4ee9197edc0d0da8b3dfda8ba9a51b3939
added simp rules

diff -r 8ff7fd4ee919 -r e034a563ed7d src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sat Jun 17 14:52:23 2017 +0200
+++ b/src/HOL/HOL.thy	Sat Jun 17 15:41:19 2017 +0200
@@ -927,6 +927,7 @@
     "\<And>P. (\<exists>x. t = x \<and> P x) = P t"
     "\<And>P. (\<forall>x. x = t \<longrightarrow> P x) = P t"
     "\<And>P. (\<forall>x. t = x \<longrightarrow> P x) = P t"
+    "(\<forall>x. x \<noteq> t) = False"  "(\<forall>x. t \<noteq> x) = False"
   by (blast, blast, blast, blast, blast, iprover+)
 
 lemma disj_absorb: "A \<or> A \<longleftrightarrow> A"