(* Title: HOLCF/IOA/Storage/ROOT.ML Author: Olaf Mueller Memory storage case study. *) goals_limit := 1; use_thys ["Correctness"];