author | haftmann |
Mon, 06 Nov 2006 16:28:31 +0100 | |
changeset 21191 | c00161fbf990 |
parent 20809 | 6c4fd0b4b63a |
child 21192 | 5fe5cd5fede7 |
permissions | -rw-r--r-- |
20809 | 1 |
(* $Id$ *) |
10253 | 2 |
(*<*) |
15131 | 3 |
theory Library |
15140 | 4 |
imports |
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
16109
diff
changeset
|
5 |
BigO |
15131 | 6 |
Continuity |
15324 | 7 |
EfficientNat |
17633 | 8 |
ExecutableSet |
19605 | 9 |
ExecutableRat |
20400 | 10 |
MLString |
15131 | 11 |
FuncSet |
12 |
Multiset |
|
13 |
NatPair |
|
14 |
Nat_Infinity |
|
15 |
Nested_Environment |
|
15470 | 16 |
OptionalSugar |
15131 | 17 |
Permutation |
18 |
Primes |
|
19 |
Quotient |
|
20 |
While_Combinator |
|
21 |
Word |
|
22 |
Zorn |
|
15731 | 23 |
Char_ord |
17516 | 24 |
Commutative_Ring |
18397 | 25 |
Coinductive_List |
19234 | 26 |
AssocList |
20809 | 27 |
Infinite_Set |
15131 | 28 |
begin |
10253 | 29 |
end |
30 |
(*>*) |