isabelle: src/HOL/BNF/BNF.thy@7f7311d04727 (annotated)

49509 163914705f8d renamed top-level theory from "Codatatype" to "BNF" blanchet parents: 49309 diff changeset	1	(* Title: HOL/BNF/BNF.thy
48975 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
49509 163914705f8d renamed top-level theory from "Codatatype" to "BNF" blanchet parents: 49309 diff changeset	7	Bounded natural functors for (co)datatypes.
48975 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
49509 163914705f8d renamed top-level theory from "Codatatype" to "BNF" blanchet parents: 49309 diff changeset	10	header {* Bounded Natural Functors for (Co)datatypes *}
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	11
49509 163914705f8d renamed top-level theory from "Codatatype" to "BNF" blanchet parents: 49309 diff changeset	12	theory BNF
49309 f20b24214ac2 split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF blanchet parents: 49308 diff changeset	13	imports More_BNFs
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	14	begin
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	15
51894 7c43b8df0f5d tuned traytel parents: 51446 diff changeset	16	hide_const (open) Gr Grp collect fsts snds setl setr
51909 eb3169abcbd5 removed dead internal constants/theorems traytel parents: 51894 diff changeset	17	convol thePull pick_middlep fstOp sndOp csquare inver
51446 a6ebb12cc003 hide internal constants; tuned proofs traytel parents: 49510 diff changeset	18	image2 relImage relInvImage prefCl PrefCl Succ Shift shift
a6ebb12cc003 hide internal constants; tuned proofs traytel parents: 49510 diff changeset	19
48975 7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	20	end

author	traytel
	Mon, 15 Jul 2013 15:50:39 +0200
changeset 52660	7f7311d04727
parent 51909	eb3169abcbd5
child 52719	480a3479fa47
permissions	-rw-r--r--