| changeset 49312 | c874ff5658dc |
| parent 49309 | f20b24214ac2 |
| child 49486 | 64cc57c0d0fe |
--- a/src/HOL/Codatatype/BNF_Wrap.thy Wed Sep 12 06:27:36 2012 +0200 +++ b/src/HOL/Codatatype/BNF_Wrap.thy Wed Sep 12 06:27:48 2012 +0200 @@ -14,6 +14,9 @@ "no_dests" begin +lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y" +by (erule iffI) (erule contrapos_pn) + ML_file "Tools/bnf_wrap_tactics.ML" ML_file "Tools/bnf_wrap.ML"