author | huffman |
Fri, 20 Feb 2009 07:41:41 -0800 | |
changeset 30018 | 690c65b8ad1a |
parent 29994 | 6ca6b6bd6e15 |
child 30019 | a2f19e0a28b2 |
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 |
24994
c385c4eabb3b
consolidated naming conventions for code generator theories
haftmann
parents:
24626
diff
changeset
|
12 |
Code_Index |
26170 | 13 |
Code_Integer |
21256 | 14 |
Coinductive_List |
15 |
Commutative_Ring |
|
15131 | 16 |
Continuity |
29026 | 17 |
ContNotDenum |
26170 | 18 |
Countable |
29847 | 19 |
Determinants |
23854 | 20 |
Efficient_Nat |
26348 | 21 |
Enum |
24281 | 22 |
Eval_Witness |
23854 | 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 |
29688 | 25 |
Formal_Power_Series |
29986 | 26 |
FrechetDeriv |
21256 | 27 |
FuncSet |
29879 | 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 | 30 |
Inner_Product |
26173 | 31 |
ListVector |
29708 | 32 |
Mapping |
15131 | 33 |
Multiset |
34 |
Nat_Infinity |
|
35 |
Nested_Environment |
|
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
24281
diff
changeset
|
36 |
Numeral_Type |
15470 | 37 |
OptionalSugar |
26232 | 38 |
Option_ord |
15131 | 39 |
Permutation |
28668
e79e196039a1
fixed and reactivated HOL/Library/Pocklington.thy -- by Mark Hillebrand;
wenzelm
parents:
28228
diff
changeset
|
40 |
Pocklington |
29985
57975b45ab70
split polynomial-related stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
29879
diff
changeset
|
41 |
Poly_Deriv |
29987 | 42 |
Polynomial |
15131 | 43 |
Primes |
30018 | 44 |
Product_plus |
29806 | 45 |
Quickcheck |
24615 | 46 |
Quicksort |
15131 | 47 |
Quotient |
21635
32f3e1127de2
added Ramsey.thy to Library imports, to include it in the daily builds
krauss
parents:
21256
diff
changeset
|
48 |
Ramsey |
29806 | 49 |
Random |
29650 | 50 |
Reflection |
26192
52617dca8386
new theory of red-black trees, an efficient implementation of finite maps.
krauss
parents:
26173
diff
changeset
|
51 |
RBT |
21256 | 52 |
State_Monad |
29504 | 53 |
Univ_Poly |
15131 | 54 |
While_Combinator |
55 |
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
|
56 |
Zorn |
15131 | 57 |
begin |
10253 | 58 |
end |
59 |
(*>*) |