isabelle: src/HOL/Library/Library.thy@8a904ff43f28 (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
27652 818666de6c24 refined code generator setup for rational numbers; more simplification rules for rational numbers haftmann parents: 27475 diff changeset	5	Abstract_Rat
21256 47195501ecf7 moved theories Parity, GCD, Binomial to Library; wenzelm parents: 21192 diff changeset	6	AssocList
16908 d374530bfaaa Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy avigad parents: 16109 diff changeset	7	BigO
21256 47195501ecf7 moved theories Parity, GCD, Binomial to Library; wenzelm parents: 21192 diff changeset	8	Binomial
24332 e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman kleing parents: 24281 diff changeset	9	Boolean_Algebra
21256 47195501ecf7 moved theories Parity, GCD, Binomial to Library; wenzelm parents: 21192 diff changeset	10	Char_ord
26170 66e6b967ccf1 added theories for imperative HOL haftmann parents: 26157 diff changeset	11	Code_Char_chr
24994 c385c4eabb3b consolidated naming conventions for code generator theories haftmann parents: 24626 diff changeset	12	Code_Index
26170 66e6b967ccf1 added theories for imperative HOL haftmann parents: 26157 diff changeset	13	Code_Integer
21256 47195501ecf7 moved theories Parity, GCD, Binomial to Library; wenzelm parents: 21192 diff changeset	14	Coinductive_List
47195501ecf7 moved theories Parity, GCD, Binomial to Library; wenzelm parents: 21192 diff changeset	15	Commutative_Ring
15131 c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	16	Continuity
29026 5fbaa05f637f moved ContNotDenum into Library nipkow parents: 28952 diff changeset	17	ContNotDenum
26170 66e6b967ccf1 added theories for imperative HOL haftmann parents: 26157 diff changeset	18	Countable
26157 4d9d0a26c32a Loads Dense_Linear_Order.thy chaieb parents: 26122 diff changeset	19	Dense_Linear_Order
23854 688a8a7bcd4e uniform naming conventions for CG theories haftmann parents: 23192 diff changeset	20	Efficient_Nat
26348 0f8e23edd357 added theory Library/Enum.thy haftmann parents: 26272 diff changeset	21	Enum
24281 7d0334b69711 added Eval_Witness theory haftmann parents: 24197 diff changeset	22	Eval_Witness
23854 688a8a7bcd4e uniform naming conventions for CG theories haftmann parents: 23192 diff changeset	23	Executable_Set
28952 15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s haftmann parents: 28668 diff changeset	24	Float
21256 47195501ecf7 moved theories Parity, GCD, Binomial to Library; wenzelm parents: 21192 diff changeset	25	FuncSet
26170 66e6b967ccf1 added theories for imperative HOL haftmann parents: 26157 diff changeset	26	Imperative_HOL
27475 61b979a2c820 add Infinite_Set and Zorn back in (since they are no longer included in main HOL image) huffman parents: 27368 diff changeset	27	Infinite_Set
26173 5cac519abe4e renamed ListSpace to ListVector; wenzelm parents: 26170 diff changeset	28	ListVector
15131 c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	29	Multiset
c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	30	Nat_Infinity
c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	31	Nested_Environment
24332 e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman kleing parents: 24281 diff changeset	32	Numeral_Type
15470 7e12ad2f6672 added OptionalSugar nipkow parents: 15324 diff changeset	33	OptionalSugar
26232 075264a0a4bc canonical order on option type haftmann parents: 26192 diff changeset	34	Option_ord
15131 c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	35	Permutation
28668 e79e196039a1 fixed and reactivated HOL/Library/Pocklington.thy -- by Mark Hillebrand; wenzelm parents: 28228 diff changeset	36	Pocklington
15131 c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	37	Primes
24615 17dbd993293d Added function package to PreList nipkow parents: 24530 diff changeset	38	Quicksort
15131 c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	39	Quotient
21635 32f3e1127de2 added Ramsey.thy to Library imports, to include it in the daily builds krauss parents: 21256 diff changeset	40	Ramsey
26192 52617dca8386 new theory of red-black trees, an efficient implementation of finite maps. krauss parents: 26173 diff changeset	41	RBT
21256 47195501ecf7 moved theories Parity, GCD, Binomial to Library; wenzelm parents: 21192 diff changeset	42	State_Monad
15131 c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	43	While_Combinator
c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	44	Word
27475 61b979a2c820 add Infinite_Set and Zorn back in (since they are no longer included in main HOL image) huffman parents: 27368 diff changeset	45	Zorn
15131 c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	46	begin
10253 73b46b18c348 "The Supplemental Isabelle/HOL Library"; wenzelm parents: diff changeset	47	end
73b46b18c348 "The Supplemental Isabelle/HOL Library"; wenzelm parents: diff changeset	48	(>)

author	wenzelm
	Tue, 16 Dec 2008 16:25:19 +0100
changeset 29120	8a904ff43f28
parent 29026	5fbaa05f637f
child 29197	6d4cb27ed19c
permissions	-rw-r--r--