isabelle: src/HOL/Library/Library.thy@52d71ee5c8a8 (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
16908 d374530bfaaa Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy avigad parents: 16109 diff changeset	4	BigO
15131 c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	5	Continuity
15324 c27165172e30 Added EfficientNat berghofe parents: 15140 diff changeset	6	EfficientNat
17633 7daaa7fe9c96 Added ExecutableSet. berghofe parents: 17516 diff changeset	7	ExecutableSet
19605 67e6b4759b37 added ExecutableRat.thy haftmann parents: 19564 diff changeset	8	ExecutableRat
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
19234 054332e39e0a Added Library/AssocList.thy schirmer parents: 19106 diff changeset	24	AssocList
15131 c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	25	begin
10253 73b46b18c348 "The Supplemental Isabelle/HOL Library"; wenzelm parents: diff changeset	26	end
73b46b18c348 "The Supplemental Isabelle/HOL Library"; wenzelm parents: diff changeset	27	(>)

author	haftmann
	Tue, 06 Jun 2006 14:55:19 +0200
changeset 19785	52d71ee5c8a8
parent 19605	67e6b4759b37
child 20400	0ad2f3bbd4f0
permissions	-rw-r--r--