src/HOL/Codatatype/BNF_Wrap.thy
author blanchet
Wed Sep 12 06:27:48 2012 +0200 (2012-09-12)
changeset 49312 c874ff5658dc
parent 49309 f20b24214ac2
child 49486 64cc57c0d0fe
permissions -rw-r--r--
moved theorems closer to where they are used
     1 (*  Title:      HOL/Codatatype/BNF_Wrap.thy
     2     Author:     Dmitriy Traytel, TU Muenchen
     3     Copyright   2012
     4 
     5 Wrapping datatypes.
     6 *)
     7 
     8 header {* Wrapping Datatypes *}
     9 
    10 theory BNF_Wrap
    11 imports BNF_Util
    12 keywords
    13   "wrap_data" :: thy_goal and
    14   "no_dests"
    15 begin
    16 
    17 lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y"
    18 by (erule iffI) (erule contrapos_pn)
    19 
    20 ML_file "Tools/bnf_wrap_tactics.ML"
    21 ML_file "Tools/bnf_wrap.ML"
    22 
    23 end