changeset 39119 | 7bfa17bcd5ee |
parent 33615 | 261abc2e3155 |
39118:12f3788be67b | 39119:7bfa17bcd5ee |
---|---|
1 (* Title: HOLCF/IOA/Storage/ROOT.ML |
1 (* Title: HOLCF/IOA/Storage/ROOT.ML |
2 Author: Olaf Mueller |
2 Author: Olaf Mueller |
3 |
3 |
4 Memory storage case study. |
4 Memory storage case study. |
5 *) |
5 *) |
6 |
|
7 goals_limit := 1; |
|
8 |
|
9 use_thys ["Correctness"]; |
6 use_thys ["Correctness"]; |