eliminated Codegen.mode in favour of explicit argument;
(* Title: HOL/HOLCF/IOA/NTP/ROOT.ML Author: Tobias Nipkow & Konrad SlindThis is the ROOT file for a network transmission protocol (NTPsubdirectory), performed in the I/O automata formalization by OlafMueller.*)use_thys ["Correctness"];