isabelle: src/HOL/Library/Library.thy@c54748fd1f43 (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
21635 32f3e1127de2 added Ramsey.thy to Library imports, to include it in the daily builds krauss parents: 21256 diff changeset	28	Ramsey
21256 47195501ecf7 moved theories Parity, GCD, Binomial to Library; wenzelm parents: 21192 diff changeset	29	State_Monad
22359 94a794672c8b Added formalization of size-change principle (experimental). krauss parents: 21635 diff changeset	30	Size_Change_Termination
15131 c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	31	While_Combinator
c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	32	Word
c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	33	Zorn
c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	34	begin
10253 73b46b18c348 "The Supplemental Isabelle/HOL Library"; wenzelm parents: diff changeset	35	end
73b46b18c348 "The Supplemental Isabelle/HOL Library"; wenzelm parents: diff changeset	36	(>)

author	urbanc
	Thu, 22 Mar 2007 11:17:32 +0100
changeset 22495	c54748fd1f43
parent 22359	94a794672c8b
child 22519	eb70ed79dac7
permissions	-rw-r--r--