| changeset 79690 | ecc851dd274f |
| parent 79689 | fabe9f89911f |
| child 79691 | d298c5b65d8e |
| 79689:fabe9f89911f | 79690:ecc851dd274f |
|---|---|
3 |
3 |
4 ML heap operations. |
4 ML heap operations. |
5 */ |
5 */ |
6 |
6 |
7 package isabelle |
7 package isabelle |
8 |
|
9 |
|
10 import java.nio.ByteBuffer |
|
11 import java.nio.channels.FileChannel |
|
12 import java.nio.file.StandardOpenOption |
|
13 |
8 |
14 |
9 |
15 object ML_Heap { |
10 object ML_Heap { |
16 /** heap file with SHA1 digest **/ |
11 /** heap file with SHA1 digest **/ |
17 |
12 |