added simp rules
authornipkow
Sat Jun 17 15:41:19 2017 +0200 (2017-06-17)
changeset 66109e034a563ed7d
parent 66103 8ff7fd4ee919
child 66110 d59f9f696110
added simp rules
src/HOL/HOL.thy
     1.1 --- a/src/HOL/HOL.thy	Sat Jun 17 14:52:23 2017 +0200
     1.2 +++ b/src/HOL/HOL.thy	Sat Jun 17 15:41:19 2017 +0200
     1.3 @@ -927,6 +927,7 @@
     1.4      "\<And>P. (\<exists>x. t = x \<and> P x) = P t"
     1.5      "\<And>P. (\<forall>x. x = t \<longrightarrow> P x) = P t"
     1.6      "\<And>P. (\<forall>x. t = x \<longrightarrow> P x) = P t"
     1.7 +    "(\<forall>x. x \<noteq> t) = False"  "(\<forall>x. t \<noteq> x) = False"
     1.8    by (blast, blast, blast, blast, blast, iprover+)
     1.9  
    1.10  lemma disj_absorb: "A \<or> A \<longleftrightarrow> A"