isabelle: src/HOL/Library/Library.thy@1d39091a3208 (annotated)

20809 6c4fd0b4b63a moved theory Infinite_Set to Library; wenzelm parents: 20400 diff changeset	1	(* $Id$ *)
10253 73b46b18c348 "The Supplemental Isabelle/HOL Library"; wenzelm parents: diff changeset	2	(<)
15131 c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	3	theory Library
15140 322485b816ac import -> imports nipkow parents: 15131 diff changeset	4	imports
21256 47195501ecf7 moved theories Parity, GCD, Binomial to Library; wenzelm parents: 21192 diff changeset	5	AssocList
16908 d374530bfaaa Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy avigad parents: 16109 diff changeset	6	BigO
21256 47195501ecf7 moved theories Parity, GCD, Binomial to Library; wenzelm parents: 21192 diff changeset	7	Binomial
47195501ecf7 moved theories Parity, GCD, Binomial to Library; wenzelm parents: 21192 diff changeset	8	Char_ord
47195501ecf7 moved theories Parity, GCD, Binomial to Library; wenzelm parents: 21192 diff changeset	9	Coinductive_List
47195501ecf7 moved theories Parity, GCD, Binomial to Library; wenzelm parents: 21192 diff changeset	10	Commutative_Ring
15131 c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	11	Continuity
15324 c27165172e30 Added EfficientNat berghofe parents: 15140 diff changeset	12	EfficientNat
21256 47195501ecf7 moved theories Parity, GCD, Binomial to Library; wenzelm parents: 21192 diff changeset	13	ExecutableRat
17633 7daaa7fe9c96 Added ExecutableSet. berghofe parents: 17516 diff changeset	14	ExecutableSet
21256 47195501ecf7 moved theories Parity, GCD, Binomial to Library; wenzelm parents: 21192 diff changeset	15	FuncSet
47195501ecf7 moved theories Parity, GCD, Binomial to Library; wenzelm parents: 21192 diff changeset	16	GCD
47195501ecf7 moved theories Parity, GCD, Binomial to Library; wenzelm parents: 21192 diff changeset	17	Infinite_Set
20400 0ad2f3bbd4f0 added some codegen examples/applications haftmann parents: 19605 diff changeset	18	MLString
15131 c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	19	Multiset
c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	20	NatPair
c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	21	Nat_Infinity
c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	22	Nested_Environment
15470 7e12ad2f6672 added OptionalSugar nipkow parents: 15324 diff changeset	23	OptionalSugar
21256 47195501ecf7 moved theories Parity, GCD, Binomial to Library; wenzelm parents: 21192 diff changeset	24	Parity
15131 c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	25	Permutation
c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	26	Primes
c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	27	Quotient
21256 47195501ecf7 moved theories Parity, GCD, Binomial to Library; wenzelm parents: 21192 diff changeset	28	State_Monad
15131 c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	29	While_Combinator
c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	30	Word
c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	31	Zorn
c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	32	begin
10253 73b46b18c348 "The Supplemental Isabelle/HOL Library"; wenzelm parents: diff changeset	33	end
73b46b18c348 "The Supplemental Isabelle/HOL Library"; wenzelm parents: diff changeset	34	(>)

author	nipkow
	Sun, 12 Nov 2006 19:22:10 +0100
changeset 21312	1d39091a3208
parent 21256	47195501ecf7
child 21635	32f3e1127de2
permissions	-rw-r--r--