isabelle: src/HOL/Library/Library.thy@c90a1f450327 (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
c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	5	Continuity
15324 c27165172e30 Added EfficientNat berghofe parents: 15140 diff changeset	6	EfficientNat
15131 c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	7	FuncSet
c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	8	Multiset
c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	9	NatPair
c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	10	Nat_Infinity
c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	11	Nested_Environment
15470 7e12ad2f6672 added OptionalSugar nipkow parents: 15324 diff changeset	12	OptionalSugar
15131 c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	13	Permutation
c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	14	Primes
c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	15	Quotient
c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	16	While_Combinator
c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	17	Word
c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	18	Zorn
16109 e8c169d6f191 Removes an inconsistent definition from Library.thy , obua parents: 15731 diff changeset	19	(List_Prefix)
15731 29ae73d8a84e Removed dir Orderings in Library nipkow parents: 15470 diff changeset	20	Char_ord
29ae73d8a84e Removed dir Orderings in Library nipkow parents: 15470 diff changeset	21	List_lexord
15131 c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	22	begin
10253 73b46b18c348 "The Supplemental Isabelle/HOL Library"; wenzelm parents: diff changeset	23	end
73b46b18c348 "The Supplemental Isabelle/HOL Library"; wenzelm parents: diff changeset	24	(>)

author	wenzelm
	Thu, 14 Jul 2005 17:16:52 +0200
changeset 16827	c90a1f450327
parent 16109	e8c169d6f191
child 16908	d374530bfaaa
permissions	-rw-r--r--