# HG changeset patch
# User paulson
# Date 1162392671 -3600
# Node ID 8a1d62375ff853b3e7e2cae68cc5b5d1842fe4fb
# Parent  85fd05aaf73711bb7424f7de0a13b6549c459ec4
clauses for iff-introduction, unfortunately useless

diff -r 85fd05aaf737 -r 8a1d62375ff8 src/HOL/Reconstruction.thy
--- a/src/HOL/Reconstruction.thy	Wed Nov 01 15:50:19 2006 +0100
+++ b/src/HOL/Reconstruction.thy	Wed Nov 01 15:51:11 2006 +0100
@@ -71,6 +71,16 @@
 apply (simp add: COMBB_def) 
 done
 
+text{*These two represent the equivalence between Boolean equality and iff.
+They can't be converted to clauses automatically, as the iff would be 
+expanded...*}
+
+lemma iff_positive: "P | Q | P=Q"
+by blast
+
+lemma iff_negative: "~P | ~Q | P=Q"
+by blast
+
 use "Tools/res_axioms.ML"
 use "Tools/res_hol_clause.ML"
 use "Tools/res_atp.ML"