isabelle: src/HOL/Library/Library.thy@958d2f2dd8d4 (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
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	kleing
	Wed, 26 Apr 2006 07:01:33 +0200
changeset 19469	958d2f2dd8d4
parent 19351	c33563c7c14c
child 19564	d3e2f532459a
permissions	-rw-r--r--