src/HOLCF/IOA/NTP/ROOT.ML
author wenzelm
Tue, 10 Jul 2007 23:29:43 +0200
changeset 23719 ccd9cb15c062
parent 19739 c58ef2aa5430
child 24584 01e83ffa6c54
permissions -rw-r--r--
more markup for inner and outer syntax; added enclose;

(*  Title:      HOL/IOA/examples/NTP/ROOT.ML
    ID:         $Id$
    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_thy "Correctness";