| changeset 9000 | c20d58286a51 |
| parent 7626 | 5997f35954d7 |
| child 9791 | a39e5d43de55 |
| 8999:ad8260dc6e4a | 9000:c20d58286a51 |
|---|---|
5 |
5 |
6 A simple model of dataflow (sub)type analysis of instruction sequences, |
6 A simple model of dataflow (sub)type analysis of instruction sequences, |
7 aka `bytecode verification'. |
7 aka `bytecode verification'. |
8 *) |
8 *) |
9 |
9 |
10 writeln"Root file for HOL/BCV"; |
|
11 |
|
12 time_use_thy "Machine"; |
10 time_use_thy "Machine"; |