isabelle: src/HOL/Library/Library.thy@07dbdf60d5ad (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
27652 818666de6c24 refined code generator setup for rational numbers; more simplification rules for rational numbers haftmann parents: 27475 diff changeset	4	Abstract_Rat
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
29994 6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library huffman parents: 29993 diff changeset	8	Bit
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
66e6b967ccf1 added theories for imperative HOL haftmann parents: 26157 diff changeset	12	Code_Integer
21256 47195501ecf7 moved theories Parity, GCD, Binomial to Library; wenzelm parents: 21192 diff changeset	13	Coinductive_List
15131 c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	14	Continuity
29026 5fbaa05f637f moved ContNotDenum into Library nipkow parents: 28952 diff changeset	15	ContNotDenum
26170 66e6b967ccf1 added theories for imperative HOL haftmann parents: 26157 diff changeset	16	Countable
30326 a01b2de0e3e1 constructive version of Cantor's first diagonalization argument haftmann parents: 30261 diff changeset	17	Diagonalize
23854 688a8a7bcd4e uniform naming conventions for CG theories haftmann parents: 23192 diff changeset	18	Efficient_Nat
26348 0f8e23edd357 added theory Library/Enum.thy haftmann parents: 26272 diff changeset	19	Enum
24281 7d0334b69711 added Eval_Witness theory haftmann parents: 24197 diff changeset	20	Eval_Witness
23854 688a8a7bcd4e uniform naming conventions for CG theories haftmann parents: 23192 diff changeset	21	Executable_Set
28952 15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s haftmann parents: 28668 diff changeset	22	Float
29688 6ed9ac8410d8 Added Formal_Power_Series in imports chaieb parents: 29650 diff changeset	23	Formal_Power_Series
31761 3585bebe49a8 Added Library/Fraction_Field.thy: The fraction field of any integral chaieb parents: 31379 diff changeset	24	Fraction_Field
29986 6b1ccda8bf19 move FrechetDeriv.thy to Library huffman parents: 29985 diff changeset	25	FrechetDeriv
31849 431d8588bcad renamed theory Code_Set to Fset haftmann parents: 31807 diff changeset	26	Fset
21256 47195501ecf7 moved theories Parity, GCD, Binomial to Library; wenzelm parents: 21192 diff changeset	27	FuncSet
29879 4425849f5db7 Moved FTA into Lib and cleaned it up a little. nipkow parents: 29847 diff changeset	28	Fundamental_Theorem_Algebra
27475 61b979a2c820 add Infinite_Set and Zorn back in (since they are no longer included in main HOL image) huffman parents: 27368 diff changeset	29	Infinite_Set
29993 84b2c432b94a new theory of real inner product spaces huffman parents: 29987 diff changeset	30	Inner_Product
35032 7efe662e41b4 separate library theory for type classes combining lattices with various algebraic structures haftmann parents: 34020 diff changeset	31	Lattice_Algebras
30326 a01b2de0e3e1 constructive version of Cantor's first diagonalization argument haftmann parents: 30261 diff changeset	32	Lattice_Syntax
26173 5cac519abe4e renamed ListSpace to ListVector; wenzelm parents: 26170 diff changeset	33	ListVector
31990 1d4d0b305f16 move Kleene_Algebra to Library krauss parents: 31849 diff changeset	34	Kleene_Algebra
29708 e40b70d38909 added Mapping.thy to Library haftmann parents: 29688 diff changeset	35	Mapping
15131 c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	36	Multiset
c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	37	Nat_Infinity
c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	38	Nested_Environment
24332 e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman kleing parents: 24281 diff changeset	39	Numeral_Type
15470 7e12ad2f6672 added OptionalSugar nipkow parents: 15324 diff changeset	40	OptionalSugar
26232 075264a0a4bc canonical order on option type haftmann parents: 26192 diff changeset	41	Option_ord
15131 c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	42	Permutation
29985 57975b45ab70 split polynomial-related stuff from Deriv.thy into Library/Poly_Deriv.thy huffman parents: 29879 diff changeset	43	Poly_Deriv
29987 391dcbd7e4dd move Polynomial.thy to Library huffman parents: 29986 diff changeset	44	Polynomial
31060 75d7c7cc8bdb added theory for explicit equivalence relation in preorders haftmann parents: 30326 diff changeset	45	Preorder
30019 a2f19e0a28b2 add theory of products as real vector spaces to Library huffman parents: 30018 diff changeset	46	Product_Vector
24615 17dbd993293d Added function package to PreList nipkow parents: 24530 diff changeset	47	Quicksort
15131 c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	48	Quotient
21635 32f3e1127de2 added Ramsey.thy to Library imports, to include it in the daily builds krauss parents: 21256 diff changeset	49	Ramsey
29650 cc3958d31b1d Reflection.thy now in HOL/Library haftmann parents: 29504 diff changeset	50	Reflection
26192 52617dca8386 new theory of red-black trees, an efficient implementation of finite maps. krauss parents: 26173 diff changeset	51	RBT
33084 cd1579e0997a turned off old quickcheck haftmann parents: 32479 diff changeset	52	SML_Quickcheck
21256 47195501ecf7 moved theories Parity, GCD, Binomial to Library; wenzelm parents: 21192 diff changeset	53	State_Monad
35029 22aab1c5e5a8 separate theory for index structures haftmann parents: 34020 diff changeset	54	Structure_Syntax
31117 527ba4a37843 Added files Sum_Of_Squares.thy, positivstellensatz.ML and sum_of_squares.ML to Library chaieb parents: 31060 diff changeset	55	Sum_Of_Squares
33649 854173fcd21c added a tabled implementation of the reflexive transitive closure bulwahn parents: 33356 diff changeset	56	Transitive_Closure_Table
29504 4c3441f2f619 moved Univ_Poly to Library haftmann parents: 29399 diff changeset	57	Univ_Poly
15131 c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	58	While_Combinator
c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	59	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	60	Zorn
15131 c69542757a4d New theory header syntax. nipkow parents: 14706 diff changeset	61	begin
10253 73b46b18c348 "The Supplemental Isabelle/HOL Library"; wenzelm parents: diff changeset	62	end
73b46b18c348 "The Supplemental Isabelle/HOL Library"; wenzelm parents: diff changeset	63	(>)

author	haftmann
	Mon, 08 Feb 2010 14:22:22 +0100
changeset 35043	07dbdf60d5ad
parent 35039	e682bb587071
child 35091	59b41ba431b5
permissions	-rw-r--r--