isabelle: src/HOLCF/IOA/NTP/ROOT.ML@e73f8140af78 (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
6597093b77e7 GPLed; wenzelm parents: 9000 diff changeset	7	M�ller.
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
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	10	goals_limit := 1;
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	11
9000 c20d58286a51 cleaned up; wenzelm parents: 6217 diff changeset	12	time_use_thy "Correctness";