isabelle: src/HOL/Library/Library.thy@2d94eb7ff17f (annotated)

10253 73b46b18c348 "The Supplemental Isabelle/HOL Library"; wenzelm parents: diff changeset	1	(<)
15131 c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	2	theory Library
15140 322485b816ac import -> imports nipkow parents: 15131 diff changeset	3	imports
15131 c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	4	Accessible_Part
16908 d374530bfaaa Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy avigad parents: 16109 diff changeset	5	BigO
15131 c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	6	Continuity
15324 c27165172e30 Added EfficientNat berghofe parents: 15140 diff changeset	7	EfficientNat
17633 7daaa7fe9c96 Added ExecutableSet. berghofe parents: 17516 diff changeset	8	ExecutableSet
15131 c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	9	FuncSet
c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	10	Multiset
c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	11	NatPair
c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	12	Nat_Infinity
c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	13	Nested_Environment
15470 7e12ad2f6672 added OptionalSugar nipkow parents: 15324 diff changeset	14	OptionalSugar
15131 c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	15	Permutation
c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	16	Primes
c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	17	Quotient
c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	18	While_Combinator
c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	19	Word
c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	20	Zorn
15731 29ae73d8a84e Removed dir Orderings in Library nipkow parents: 15470 diff changeset	21	Char_ord
17516 45164074dad4 added Commutative_Ring (from Main HOL); wenzelm parents: 16966 diff changeset	22	Commutative_Ring
18397 2d94eb7ff17f added HOL/Library/Coinductive_List.thy; wenzelm parents: 17633 diff changeset	23	Coinductive_List
15131 c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	24	begin
10253 73b46b18c348 "The Supplemental Isabelle/HOL Library"; wenzelm parents: diff changeset	25	end
73b46b18c348 "The Supplemental Isabelle/HOL Library"; wenzelm parents: diff changeset	26	(>)

author	wenzelm
	Tue, 13 Dec 2005 19:32:04 +0100
changeset 18397	2d94eb7ff17f
parent 17633	7daaa7fe9c96
child 19106	6e6b5b1fdc06
permissions	-rw-r--r--