author | chaieb |
Mon, 25 Feb 2008 11:27:08 +0100 | |
changeset 26122 | 76cbf193c09d |
parent 25899 | f344ff9e2041 |
child 26157 | 4d9d0a26c32a |
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 |
24994
c385c4eabb3b
consolidated naming conventions for code generator theories
haftmann
parents:
24626
diff
changeset
|
11 |
Code_Index |
c385c4eabb3b
consolidated naming conventions for code generator theories
haftmann
parents:
24626
diff
changeset
|
12 |
Code_Message |
21256 | 13 |
Coinductive_List |
14 |
Commutative_Ring |
|
15131 | 15 |
Continuity |
23854 | 16 |
Efficient_Nat |
24626
85eceef2edc7
introduced generic concepts for theory interpretators
haftmann
parents:
24615
diff
changeset
|
17 |
(*Eval*) |
24281 | 18 |
Eval_Witness |
23854 | 19 |
Executable_Set |
21256 | 20 |
FuncSet |
21 |
GCD |
|
22 |
Infinite_Set |
|
25899 | 23 |
ListSpace |
15131 | 24 |
Multiset |
25 |
NatPair |
|
26 |
Nat_Infinity |
|
27 |
Nested_Environment |
|
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
24281
diff
changeset
|
28 |
Numeral_Type |
15470 | 29 |
OptionalSugar |
21256 | 30 |
Parity |
15131 | 31 |
Permutation |
24994
c385c4eabb3b
consolidated naming conventions for code generator theories
haftmann
parents:
24626
diff
changeset
|
32 |
Code_Integer |
c385c4eabb3b
consolidated naming conventions for code generator theories
haftmann
parents:
24626
diff
changeset
|
33 |
Code_Char_chr |
15131 | 34 |
Primes |
24615 | 35 |
Quicksort |
15131 | 36 |
Quotient |
21635
32f3e1127de2
added Ramsey.thy to Library imports, to include it in the daily builds
krauss
parents:
21256
diff
changeset
|
37 |
Ramsey |
21256 | 38 |
State_Monad |
26122 | 39 |
Univ_Poly |
15131 | 40 |
While_Combinator |
41 |
Word |
|
42 |
Zorn |
|
43 |
begin |
|
10253 | 44 |
end |
45 |
(*>*) |