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