src/HOL/Codatatype/BNF_Wrap.thy
author blanchet
Tue Sep 11 18:39:47 2012 +0200 (2012-09-11)
changeset 49286 dde4967c9233
parent 49283 97809ae5f7bb
child 49309 f20b24214ac2
permissions -rw-r--r--
added "defaults" 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_Util
    12 keywords
    13   "wrap_data" :: thy_goal and
    14   "no_dests"
    15 uses
    16   "Tools/bnf_wrap_tactics.ML"
    17   "Tools/bnf_wrap.ML"
    18 begin
    19 
    20 end