1 (* Title: HOLCF/IOA/Storage/ROOT.ML
2 ID: $Id$
3 Author: Olaf Mueller
4
5 Memory storage case study.
6 *)
7
8 goals_limit := 1;
9
10 time_use_thy "Correctness";