isabelle: src/HOL/Codatatype/Codatatype.thy@30916e44d828 (annotated)

48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	1	(* Title: HOL/Codatatype/Codatatype.thy
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	2	Author: Dmitriy Traytel, TU Muenchen
49017 66fc7fc2d49b started work on datatype sugar blanchet parents: 48975 diff changeset	3	Author: Andrei Popescu, TU Muenchen
66fc7fc2d49b started work on datatype sugar blanchet parents: 48975 diff changeset	4	Author: Jasmin Blanchette, TU Muenchen
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	5	Copyright 2012
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	6
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	7	The (co)datatype package.
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	8	*)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	9
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	10	header {* The (Co)datatype Package *}
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	11
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	12	theory Codatatype
49283 97809ae5f7bb move "bnf_util.ML" to "BNF_Util.thy" blanchet parents: 49123 diff changeset	13	imports BNF_LFP BNF_GFP BNF_Wrap
49112 4de4635d8f93 started work on sugared "(co)data" commands blanchet parents: 49075 diff changeset	14	keywords
49286 dde4967c9233 added "defaults" option blanchet parents: 49283 diff changeset	15	"data" :: thy_decl and
dde4967c9233 added "defaults" option blanchet parents: 49283 diff changeset	16	"codata" :: thy_decl and
dde4967c9233 added "defaults" option blanchet parents: 49283 diff changeset	17	"defaults"
49112 4de4635d8f93 started work on sugared "(co)data" commands blanchet parents: 49075 diff changeset	18	uses
49123 263b0e330d8b more work on sugar + simplify Trueprop + eq idiom everywhere blanchet parents: 49112 diff changeset	19	"Tools/bnf_fp_sugar_tactics.ML"
49112 4de4635d8f93 started work on sugared "(co)data" commands blanchet parents: 49075 diff changeset	20	"Tools/bnf_fp_sugar.ML"
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	21	begin
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	22
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	23	end

author	blanchet
	Wed, 12 Sep 2012 02:06:31 +0200
changeset 49307	30916e44d828
parent 49286	dde4967c9233
child 49308	6190b701e4f4
permissions	-rw-r--r--