author | haftmann |
Fri, 07 Mar 2008 13:53:01 +0100 | |
changeset 26232 | 075264a0a4bc |
parent 26192 | 52617dca8386 |
child 26272 | d63776c3be97 |
permissions | -rw-r--r-- |
20809 | 1 |
(* $Id$ *) |
10253 | 2 |
(*<*) |
15131 | 3 |
theory Library |
15140 | 4 |
imports |
24197 | 5 |
Abstract_Rat |
21256 | 6 |
AssocList |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
16109
diff
changeset
|
7 |
BigO |
21256 | 8 |
Binomial |
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 |
24994
c385c4eabb3b
consolidated naming conventions for code generator theories
haftmann
parents:
24626
diff
changeset
|
14 |
Code_Message |
21256 | 15 |
Coinductive_List |
16 |
Commutative_Ring |
|
15131 | 17 |
Continuity |
26170 | 18 |
Countable |
26157 | 19 |
Dense_Linear_Order |
23854 | 20 |
Efficient_Nat |
26170 | 21 |
Eval |
24281 | 22 |
Eval_Witness |
23854 | 23 |
Executable_Set |
21256 | 24 |
FuncSet |
25 |
GCD |
|
26170 | 26 |
Imperative_HOL |
21256 | 27 |
Infinite_Set |
26173 | 28 |
ListVector |
15131 | 29 |
Multiset |
30 |
NatPair |
|
31 |
Nat_Infinity |
|
32 |
Nested_Environment |
|
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
24281
diff
changeset
|
33 |
Numeral_Type |
15470 | 34 |
OptionalSugar |
26232 | 35 |
Option_ord |
21256 | 36 |
Parity |
15131 | 37 |
Permutation |
38 |
Primes |
|
24615 | 39 |
Quicksort |
15131 | 40 |
Quotient |
21635
32f3e1127de2
added Ramsey.thy to Library imports, to include it in the daily builds
krauss
parents:
21256
diff
changeset
|
41 |
Ramsey |
26192
52617dca8386
new theory of red-black trees, an efficient implementation of finite maps.
krauss
parents:
26173
diff
changeset
|
42 |
RBT |
21256 | 43 |
State_Monad |
26122 | 44 |
Univ_Poly |
15131 | 45 |
While_Combinator |
46 |
Word |
|
47 |
Zorn |
|
48 |
begin |
|
10253 | 49 |
end |
50 |
(*>*) |