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