author | haftmann |
Mon, 26 Mar 2007 14:53:07 +0200 | |
changeset 22524 | f9bf5c08b446 |
parent 22519 | eb70ed79dac7 |
child 22799 | ed7d53db2170 |
permissions | -rw-r--r-- |
20809 | 1 |
(* $Id$ *) |
10253 | 2 |
(*<*) |
15131 | 3 |
theory Library |
15140 | 4 |
imports |
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 |
8 |
Char_ord |
|
9 |
Coinductive_List |
|
10 |
Commutative_Ring |
|
15131 | 11 |
Continuity |
15324 | 12 |
EfficientNat |
22519 | 13 |
Eval |
21256 | 14 |
ExecutableRat |
17633 | 15 |
ExecutableSet |
21256 | 16 |
FuncSet |
17 |
GCD |
|
18 |
Infinite_Set |
|
20400 | 19 |
MLString |
15131 | 20 |
Multiset |
21 |
NatPair |
|
22 |
Nat_Infinity |
|
23 |
Nested_Environment |
|
15470 | 24 |
OptionalSugar |
21256 | 25 |
Parity |
15131 | 26 |
Permutation |
27 |
Primes |
|
28 |
Quotient |
|
21635
32f3e1127de2
added Ramsey.thy to Library imports, to include it in the daily builds
krauss
parents:
21256
diff
changeset
|
29 |
Ramsey |
21256 | 30 |
State_Monad |
22359
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
21635
diff
changeset
|
31 |
Size_Change_Termination |
15131 | 32 |
While_Combinator |
33 |
Word |
|
34 |
Zorn |
|
35 |
begin |
|
10253 | 36 |
end |
37 |
(*>*) |