isabelle: src/HOL/BNF/BNF.thy@a96bd08258a2 (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
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei) blanchet parents: diff changeset	16	end

author	wenzelm
	Tue, 20 Nov 2012 22:52:04 +0100
changeset 50136	a96bd08258a2
parent 49510	ba50d204095e
child 51446	a6ebb12cc003
permissions	-rw-r--r--