--- a/src/HOL/Sledgehammer.thy Thu Jun 24 17:27:18 2010 +0200
+++ b/src/HOL/Sledgehammer.thy Thu Jun 24 17:57:36 2010 +0200
@@ -53,16 +53,6 @@
lemma equal_imp_fequal [no_atp]: "X = Y \<Longrightarrow> fequal X Y"
by (simp add: fequal_def)
-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 \<or> Q \<or> P = Q"
-by blast
-
-lemma iff_negative: "\<not> P \<or> \<not> Q \<or> P = Q"
-by blast
-
text{*Theorems for translation to combinators*}
lemma abs_S [no_atp]: "\<lambda>x. (f x) (g x) \<equiv> COMBS f g"