| changeset 39347 | 50dec19e682b |
| parent 39346 | d837998f1e60 |
| child 39348 | 6f9c9899f99f |
| 39346:d837998f1e60 | 39347:50dec19e682b |
|---|---|
1 (* ========================================================================= *) |
|
2 (* FINITE MAPS *) |
|
3 (* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *) |
|
4 (* ========================================================================= *) |
|
5 |
|
6 structure Map = RandomMap; |