isabelle: src/HOLCF/IOA/NTP/ROOT.ML@ae1daa601638 (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
12218 6597093b77e7 GPLed; wenzelm parents: 9000 diff changeset	4	License: GPL (GNU GENERAL PUBLIC LICENSE)
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	5
12218 6597093b77e7 GPLed; wenzelm parents: 9000 diff changeset	6	This is the ROOT file for a network transmission protocol (NTP
6597093b77e7 GPLed; wenzelm parents: 9000 diff changeset	7	subdirectory), performed in the I/O automata formalization by Olaf
6597093b77e7 GPLed; wenzelm parents: 9000 diff changeset	8	M�ller.
3073 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
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	11	goals_limit := 1;
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	12
9000 c20d58286a51 cleaned up; wenzelm parents: 6217 diff changeset	13	time_use_thy "Correctness";

author	aspinall
	Thu, 10 Jun 2004 18:46:35 +0200
changeset 14916	ae1daa601638
parent 12218	6597093b77e7
child 14981	e73f8140af78
permissions	-rw-r--r--