author | hoelzl |
Thu, 01 Jul 2010 11:48:42 +0200 | |
changeset 37665 | 579258a77fec |
parent 37023 | efc202e1677e |
child 37693 | b10444eb9c98 |
permissions | -rw-r--r-- |
10253 | 1 |
(*<*) |
15131 | 2 |
theory Library |
15140 | 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 | 5 |
AssocList |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
16109
diff
changeset
|
6 |
BigO |
21256 | 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 | 10 |
Char_ord |
26170 | 11 |
Code_Char_chr |
12 |
Code_Integer |
|
15131 | 13 |
Continuity |
29026 | 14 |
ContNotDenum |
36648 | 15 |
Convex |
26170 | 16 |
Countable |
30326
a01b2de0e3e1
constructive version of Cantor's first diagonalization argument
haftmann
parents:
30261
diff
changeset
|
17 |
Diagonalize |
35303 | 18 |
Dlist |
23854 | 19 |
Efficient_Nat |
26348 | 20 |
Enum |
24281 | 21 |
Eval_Witness |
23854 | 22 |
Executable_Set |
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28668
diff
changeset
|
23 |
Float |
29688 | 24 |
Formal_Power_Series |
31761
3585bebe49a8
Added Library/Fraction_Field.thy: The fraction field of any integral
chaieb
parents:
31379
diff
changeset
|
25 |
Fraction_Field |
29986 | 26 |
FrechetDeriv |
31849 | 27 |
Fset |
21256 | 28 |
FuncSet |
29879 | 29 |
Fundamental_Theorem_Algebra |
37665 | 30 |
Indicator_Function |
27475
61b979a2c820
add Infinite_Set and Zorn back in (since they are no longer included in main HOL image)
huffman
parents:
27368
diff
changeset
|
31 |
Infinite_Set |
29993 | 32 |
Inner_Product |
35032
7efe662e41b4
separate library theory for type classes combining lattices with various algebraic structures
haftmann
parents:
34020
diff
changeset
|
33 |
Lattice_Algebras |
30326
a01b2de0e3e1
constructive version of Cantor's first diagonalization argument
haftmann
parents:
30261
diff
changeset
|
34 |
Lattice_Syntax |
26173 | 35 |
ListVector |
31990 | 36 |
Kleene_Algebra |
29708 | 37 |
Mapping |
37023 | 38 |
More_List |
15131 | 39 |
Multiset |
40 |
Nat_Infinity |
|
41 |
Nested_Environment |
|
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
24281
diff
changeset
|
42 |
Numeral_Type |
15470 | 43 |
OptionalSugar |
26232 | 44 |
Option_ord |
15131 | 45 |
Permutation |
29985
57975b45ab70
split polynomial-related stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
29879
diff
changeset
|
46 |
Poly_Deriv |
29987 | 47 |
Polynomial |
31060
75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
30326
diff
changeset
|
48 |
Preorder |
30019
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
30018
diff
changeset
|
49 |
Product_Vector |
24615 | 50 |
Quicksort |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35100
diff
changeset
|
51 |
Quotient_List |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35100
diff
changeset
|
52 |
Quotient_Option |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35100
diff
changeset
|
53 |
Quotient_Product |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35100
diff
changeset
|
54 |
Quotient_Sum |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35100
diff
changeset
|
55 |
Quotient_Syntax |
35100
53754ec7360b
renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid clash with new theory Quotient in Main HOL;
wenzelm
parents:
35091
diff
changeset
|
56 |
Quotient_Type |
21635
32f3e1127de2
added Ramsey.thy to Library imports, to include it in the daily builds
krauss
parents:
21256
diff
changeset
|
57 |
Ramsey |
29650 | 58 |
Reflection |
26192
52617dca8386
new theory of red-black trees, an efficient implementation of finite maps.
krauss
parents:
26173
diff
changeset
|
59 |
RBT |
33084 | 60 |
SML_Quickcheck |
21256 | 61 |
State_Monad |
31117
527ba4a37843
Added files Sum_Of_Squares.thy, positivstellensatz.ML and sum_of_squares.ML to Library
chaieb
parents:
31060
diff
changeset
|
62 |
Sum_Of_Squares |
33649
854173fcd21c
added a tabled implementation of the reflexive transitive closure
bulwahn
parents:
33356
diff
changeset
|
63 |
Transitive_Closure_Table |
29504 | 64 |
Univ_Poly |
15131 | 65 |
While_Combinator |
27475
61b979a2c820
add Infinite_Set and Zorn back in (since they are no longer included in main HOL image)
huffman
parents:
27368
diff
changeset
|
66 |
Zorn |
15131 | 67 |
begin |
10253 | 68 |
end |
69 |
(*>*) |