src/HOL/SMT.thy
changeset 59037 650dcf624729
parent 59036 ce58eb744e38
child 59045 1da9b8045026
     1.1 --- a/src/HOL/SMT.thy	Mon Nov 24 12:35:13 2014 +0100
     1.2 +++ b/src/HOL/SMT.thy	Mon Nov 24 12:35:13 2014 +0100
     1.3 @@ -344,6 +344,7 @@
     1.4    "(P \<longrightarrow> True) = True"
     1.5    "(False \<longrightarrow> P) = True"
     1.6    "(P \<longrightarrow> P) = True"
     1.7 +  "(\<not> (A \<longleftrightarrow> \<not> B)) \<longleftrightarrow> (A \<longleftrightarrow> B)"
     1.8    by auto
     1.9  
    1.10  lemma [z3_rule]: