(* Title: HOLCF/IOA/Storage/ROOT.ML ID: $Id$ Author: Olaf Mueller Memory storage case study. *) goals_limit := 1; time_use_thy "Correctness";