| changeset 33615 | 261abc2e3155 |
| parent 24584 | 01e83ffa6c54 |
| child 39119 | 7bfa17bcd5ee |
| 33608:5c0024338cef | 33615:261abc2e3155 |
|---|---|
1 (* Title: HOLCF/IOA/Storage/ROOT.ML |
1 (* Title: HOLCF/IOA/Storage/ROOT.ML |
2 ID: $Id$ |
|
3 Author: Olaf Mueller |
2 Author: Olaf Mueller |
4 |
3 |
5 Memory storage case study. |
4 Memory storage case study. |
6 *) |
5 *) |
7 |
6 |
8 goals_limit := 1; |
7 goals_limit := 1; |
9 |
8 |
10 time_use_thy "Correctness"; |
9 use_thys ["Correctness"]; |