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