| author | nipkow | 
| Mon, 16 Aug 2004 14:21:54 +0200 | |
| changeset 15130 | dc6be28d7f4e | 
| parent 14706 | 71590b7733b7 | 
| 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: 
11055diff
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: 
11368diff
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: 
14365diff
changeset | 15 | Word + | 
| 14706 | 16 | Zorn: | 
| 10253 | 17 | end | 
| 18 | (*>*) |