src/HOL/Codatatype/BNF_Wrap.thy
author blanchet
Tue Sep 11 14:51:52 2012 +0200 (2012-09-11)
changeset 49278 718e4ad1517e
parent 49075 ed769978dc8d
child 49283 97809ae5f7bb
permissions -rw-r--r--
added no_dests option
     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_Def
    12 keywords
    13   "wrap_data" :: thy_goal
    14 and
    15   "no_dests"
    16 uses
    17   "Tools/bnf_wrap_tactics.ML"
    18   "Tools/bnf_wrap.ML"
    19 begin
    20 
    21 end