author | avigad |
Mon, 25 Jul 2005 18:54:49 +0200 | |
changeset 16908 | d374530bfaaa |
parent 16109 | e8c169d6f191 |
child 16966 | 37e34f315057 |
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 |
15131 | 8 |
FuncSet |
9 |
Multiset |
|
10 |
NatPair |
|
11 |
Nat_Infinity |
|
12 |
Nested_Environment |
|
15470 | 13 |
OptionalSugar |
15131 | 14 |
Permutation |
15 |
Primes |
|
16 |
Quotient |
|
17 |
While_Combinator |
|
18 |
Word |
|
19 |
Zorn |
|
16109
e8c169d6f191
Removes an inconsistent definition from Library.thy ,
obua
parents:
15731
diff
changeset
|
20 |
(*List_Prefix*) |
15731 | 21 |
Char_ord |
22 |
List_lexord |
|
15131 | 23 |
begin |
10253 | 24 |
end |
25 |
(*>*) |