(* Title: HOLCF/IOA/NTP/ROOT.ML Author: Tobias Nipkow & Konrad Slind This is the ROOT file for a network transmission protocol (NTP subdirectory), performed in the I/O automata formalization by Olaf Mueller. *) use_thys ["Correctness"];