isabelle: src/HOL/Codatatype/BNF_Wrap.thy@c874ff5658dc (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
49283 97809ae5f7bb move "bnf_util.ML" to "BNF_Util.thy" blanchet parents: 49278 diff changeset	11	imports BNF_Util
49075 ed769978dc8d rearrange dependencies blanchet parents: diff changeset	12	keywords
49286 dde4967c9233 added "defaults" option blanchet parents: 49283 diff changeset	13	"wrap_data" :: thy_goal and
49278 718e4ad1517e added no_dests option blanchet parents: 49075 diff changeset	14	"no_dests"
49075 ed769978dc8d rearrange dependencies blanchet parents: diff changeset	15	begin
ed769978dc8d rearrange dependencies blanchet parents: diff changeset	16
49312 c874ff5658dc moved theorems closer to where they are used blanchet parents: 49309 diff changeset	17	lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y"
c874ff5658dc moved theorems closer to where they are used blanchet parents: 49309 diff changeset	18	by (erule iffI) (erule contrapos_pn)
c874ff5658dc moved theorems closer to where they are used blanchet parents: 49309 diff changeset	19
49309 f20b24214ac2 split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF blanchet parents: 49286 diff changeset	20	ML_file "Tools/bnf_wrap_tactics.ML"
f20b24214ac2 split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF blanchet parents: 49286 diff changeset	21	ML_file "Tools/bnf_wrap.ML"
f20b24214ac2 split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF blanchet parents: 49286 diff changeset	22
49075 ed769978dc8d rearrange dependencies blanchet parents: diff changeset	23	end

author	blanchet
	Wed, 12 Sep 2012 06:27:48 +0200
changeset 49312	c874ff5658dc
parent 49309	f20b24214ac2
child 49486	64cc57c0d0fe
permissions	-rw-r--r--