isabelle: src/HOLCF/IOA/NTP/ROOT.ML@c58ef2aa5430 (annotated)

3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	1	(* Title: HOL/IOA/examples/NTP/ROOT.ML
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	2	ID: $Id$
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	3	Author: Tobias Nipkow & Konrad Slind
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	4
12218 6597093b77e7 GPLed; wenzelm parents: 9000 diff changeset	5	This is the ROOT file for a network transmission protocol (NTP
6597093b77e7 GPLed; wenzelm parents: 9000 diff changeset	6	subdirectory), performed in the I/O automata formalization by Olaf
19360 f47412f922ab converted Müller to Mueller to make smlnj 110.58 work kleing parents: 14981 diff changeset	7	Mueller.
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	8	*)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	9
19739 c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 19360 diff changeset	10	use_thy "Correctness";