# HG changeset patch
# User blanchet
# Date 1416828913 -3600
# Node ID 650dcf62472990687d0d7086633f61153294da7d
# Parent  ce58eb744e383b4140bee27bd32f729f241823fd
added Z3 reconstruction rule suggested by F. Maric

diff -r ce58eb744e38 -r 650dcf624729 src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Mon Nov 24 12:35:13 2014 +0100
+++ b/src/HOL/SMT.thy	Mon Nov 24 12:35:13 2014 +0100
@@ -344,6 +344,7 @@
   "(P \<longrightarrow> True) = True"
   "(False \<longrightarrow> P) = True"
   "(P \<longrightarrow> P) = True"
+  "(\<not> (A \<longleftrightarrow> \<not> B)) \<longleftrightarrow> (A \<longleftrightarrow> B)"
   by auto
 
 lemma [z3_rule]: