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