src/HOL/Codatatype/BNF_Wrap.thy
changeset 49283 97809ae5f7bb
parent 49278 718e4ad1517e
child 49286 dde4967c9233
equal deleted inserted replaced
49282:c057e1b39f16 49283:97809ae5f7bb
     6 *)
     6 *)
     7 
     7 
     8 header {* Wrapping Datatypes *}
     8 header {* Wrapping Datatypes *}
     9 
     9 
    10 theory BNF_Wrap
    10 theory BNF_Wrap
    11 imports BNF_Def
    11 imports BNF_Util
    12 keywords
    12 keywords
    13   "wrap_data" :: thy_goal
    13   "wrap_data" :: thy_goal
    14 and
    14 and
    15   "no_dests"
    15   "no_dests"
    16 uses
    16 uses