(* Title: HOL/IOA/Storage/ROOT.ML ID: $Id$ Author: Olaf Mueller Copyright 1998 TU Muenchen Memory storage case study. *) goals_limit := 1; use_thy "Correctness";