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