isabelle: src/HOL/BNF/BNF.thy@2df6ad1dbd66 (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
54601 91a1e4aa7c80 command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it traytel parents: 54540 diff changeset	13	imports Countable_Set_Type BNF_LFP BNF_GFP BNF_Decl
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
52731 dacd47a0633f transfer rule for {c,d}tor_{,un}fold traytel parents: 52719 diff changeset	16	hide_const (open) image2 image2p vimage2p Gr Grp collect fsts snds setl setr
54841 af71b753c459 express weak pullback property of bnfs only in terms of the relator traytel parents: 54601 diff changeset	17	convol pick_middlep fstOp sndOp csquare inver relImage relInvImage
af71b753c459 express weak pullback property of bnfs only in terms of the relator traytel parents: 54601 diff changeset	18	prefCl PrefCl Succ Shift shift
51446 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	blanchet
	Thu, 16 Jan 2014 16:20:17 +0100
changeset 55017	2df6ad1dbd66
parent 54841	af71b753c459
child 55024	05cc0dbf3a50
permissions	-rw-r--r--