isabelle: src/HOL/BNF/BNF.thy@b1d955791529 (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
54026 82d9b2701a03 new coinduction method traytel parents: 53124 diff changeset	13	imports More_BNFs BNF_LFP BNF_GFP Coinduction
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
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	haftmann
	Fri, 01 Nov 2013 18:51:14 +0100
changeset 54230	b1d955791529
parent 54026	82d9b2701a03
child 54539	bbab2ebda234
permissions	-rw-r--r--