author | wenzelm |
Thu, 06 May 2004 14:14:18 +0200 | |
changeset 14706 | 71590b7733b7 |
parent 14494 | 48ae8d678d88 |
child 15131 | c69542757a4d |
permissions | -rw-r--r-- |
10253 | 1 |
(*<*) |
2 |
theory Library = |
|
3 |
Accessible_Part + |
|
11349
fcb507c945c3
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
11055
diff
changeset
|
4 |
Continuity + |
14706 | 5 |
FuncSet + |
6 |
List_Prefix + |
|
10253 | 7 |
Multiset + |
14127
40a4768c8e0b
new theory NatPair of the injection from nat*nat -> nat
paulson
parents:
11368
diff
changeset
|
8 |
NatPair + |
14706 | 9 |
Nat_Infinity + |
10 |
Nested_Environment + |
|
11 |
Permutation + |
|
11368 | 12 |
Primes + |
14706 | 13 |
Quotient + |
14 |
While_Combinator + |
|
14494
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
14365
diff
changeset
|
15 |
Word + |
14706 | 16 |
Zorn: |
10253 | 17 |
end |
18 |
(*>*) |