isabelle: src/HOL/Codatatype/BNF_Wrap.thy@718e4ad1517e (annotated)

49075 ed769978dc8d rearrange dependencies blanchet parents: diff changeset	1	(* Title: HOL/Codatatype/BNF_Wrap.thy
ed769978dc8d rearrange dependencies blanchet parents: diff changeset	2	Author: Dmitriy Traytel, TU Muenchen
ed769978dc8d rearrange dependencies blanchet parents: diff changeset	3	Copyright 2012
ed769978dc8d rearrange dependencies blanchet parents: diff changeset	4
ed769978dc8d rearrange dependencies blanchet parents: diff changeset	5	Wrapping datatypes.
ed769978dc8d rearrange dependencies blanchet parents: diff changeset	6	*)
ed769978dc8d rearrange dependencies blanchet parents: diff changeset	7
ed769978dc8d rearrange dependencies blanchet parents: diff changeset	8	header {* Wrapping Datatypes *}
ed769978dc8d rearrange dependencies blanchet parents: diff changeset	9
ed769978dc8d rearrange dependencies blanchet parents: diff changeset	10	theory BNF_Wrap
ed769978dc8d rearrange dependencies blanchet parents: diff changeset	11	imports BNF_Def
ed769978dc8d rearrange dependencies blanchet parents: diff changeset	12	keywords
ed769978dc8d rearrange dependencies blanchet parents: diff changeset	13	"wrap_data" :: thy_goal
49278 718e4ad1517e added no_dests option blanchet parents: 49075 diff changeset	14	and
718e4ad1517e added no_dests option blanchet parents: 49075 diff changeset	15	"no_dests"
49075 ed769978dc8d rearrange dependencies blanchet parents: diff changeset	16	uses
ed769978dc8d rearrange dependencies blanchet parents: diff changeset	17	"Tools/bnf_wrap_tactics.ML"
ed769978dc8d rearrange dependencies blanchet parents: diff changeset	18	"Tools/bnf_wrap.ML"
ed769978dc8d rearrange dependencies blanchet parents: diff changeset	19	begin
ed769978dc8d rearrange dependencies blanchet parents: diff changeset	20
ed769978dc8d rearrange dependencies blanchet parents: diff changeset	21	end

author	blanchet
	Tue, 11 Sep 2012 14:51:52 +0200
changeset 49278	718e4ad1517e
parent 49075	ed769978dc8d
child 49283	97809ae5f7bb
permissions	-rw-r--r--