src/HOL/Sledgehammer.thy
changeset 37541 a76ace919f1c
parent 37511 26afa11a1fb2
child 37569 931f5948a32d
     1.1 --- a/src/HOL/Sledgehammer.thy	Thu Jun 24 17:27:18 2010 +0200
     1.2 +++ b/src/HOL/Sledgehammer.thy	Thu Jun 24 17:57:36 2010 +0200
     1.3 @@ -53,16 +53,6 @@
     1.4  lemma equal_imp_fequal [no_atp]: "X = Y \<Longrightarrow> fequal X Y"
     1.5    by (simp add: fequal_def)
     1.6  
     1.7 -text{*These two represent the equivalence between Boolean equality and iff.
     1.8 -They can't be converted to clauses automatically, as the iff would be
     1.9 -expanded...*}
    1.10 -
    1.11 -lemma iff_positive: "P \<or> Q \<or> P = Q"
    1.12 -by blast
    1.13 -
    1.14 -lemma iff_negative: "\<not> P \<or> \<not> Q \<or> P = Q"
    1.15 -by blast
    1.16 -
    1.17  text{*Theorems for translation to combinators*}
    1.18  
    1.19  lemma abs_S [no_atp]: "\<lambda>x. (f x) (g x) \<equiv> COMBS f g"