1
(* Title: HOL/IOA/Storage/ROOT.ML
2
ID: $Id$
3
Author: Olaf Müller
4
License: GPL (GNU GENERAL PUBLIC LICENSE)
5
6
Memory storage case study.
7
*)
8
9
goals_limit := 1;
10
11
time_use_thy "Correctness";