Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added Z3 reconstruction rule suggested by F. Maric
authorblanchet
Mon, 24 Nov 2014 12:35:13 +0100
changeset 59037 650dcf624729
parent 59036 ce58eb744e38
child 59038 e50f1973cb0a
added Z3 reconstruction rule suggested by F. Maric
src/HOL/SMT.thy file | annotate | diff | comparison | revisions 
--- 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]:
isabelle