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
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@49075
    11
imports BNF_Def
blanchet@49075
    12
keywords
blanchet@49075
    13
  "wrap_data" :: thy_goal
blanchet@49278
    14
and
blanchet@49278
    15
  "no_dests"
blanchet@49075
    16
uses
blanchet@49075
    17
  "Tools/bnf_wrap_tactics.ML"
blanchet@49075
    18
  "Tools/bnf_wrap.ML"
blanchet@49075
    19
begin
blanchet@49075
    20
blanchet@49075
    21
end