author | nipkow |
Thu, 23 Mar 2006 20:03:53 +0100 | |
changeset 19323 | ec5cd5b1804c |
parent 19234 | 054332e39e0a |
child 19351 | c33563c7c14c |
permissions | -rw-r--r-- |
10253 | 1 |
(*<*) |
15131 | 2 |
theory Library |
15140 | 3 |
imports |
15131 | 4 |
Accessible_Part |
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 |
15131 | 9 |
FuncSet |
10 |
Multiset |
|
11 |
NatPair |
|
12 |
Nat_Infinity |
|
13 |
Nested_Environment |
|
15470 | 14 |
OptionalSugar |
15131 | 15 |
Permutation |
16 |
Primes |
|
17 |
Quotient |
|
18 |
While_Combinator |
|
19 |
Word |
|
20 |
Zorn |
|
15731 | 21 |
Char_ord |
17516 | 22 |
Commutative_Ring |
18397 | 23 |
Coinductive_List |
19106
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
18397
diff
changeset
|
24 |
ASeries |
19234 | 25 |
AssocList |
15131 | 26 |
begin |
10253 | 27 |
end |
28 |
(*>*) |