added Z3 reconstruction rule suggested by F. Maric
authorblanchet
Mon Nov 24 12:35:13 2014 +0100 (2014-11-24)
changeset 59037650dcf624729
parent 59036 ce58eb744e38
child 59038 e50f1973cb0a
added Z3 reconstruction rule suggested by F. Maric
src/HOL/SMT.thy
     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]: