src/HOL/HOLCF/IOA/NTP/ROOT.ML
author wenzelm
Tue, 19 Apr 2011 23:57:28 +0200
changeset 42411 ff997038e8eb
parent 42151 4da4fc77664b
permissions -rw-r--r--
eliminated Codegen.mode in favour of explicit argument;

(*  Title:      HOL/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"];