isabelle: src/HOL/HOLCF/IOA/NTP/ROOT.ML@6d736d983d5c (annotated)

24584 01e83ffa6c54 fixed title haftmann parents: 19739 diff changeset	1	(* Title: HOLCF/IOA/NTP/ROOT.ML
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	2	Author: Tobias Nipkow & Konrad Slind
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	3
12218 6597093b77e7 GPLed; wenzelm parents: 9000 diff changeset	4	This is the ROOT file for a network transmission protocol (NTP
6597093b77e7 GPLed; wenzelm parents: 9000 diff changeset	5	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	6	Mueller.
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	7	*)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	8
33615 261abc2e3155 uniform use of simultabeous use_thys; wenzelm parents: 24584 diff changeset	9	use_thys ["Correctness"];