src/HOLCF/IOA/NTP/ROOT.ML
author wenzelm
Wed, 01 Oct 2008 20:02:37 +0200
changeset 28451 0586b855c2b5
parent 24584 01e83ffa6c54
child 33615 261abc2e3155
permissions -rw-r--r--
datatype transition: internal trans field is maintained in reverse order; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
    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
wenzelm
parents: 9000
diff changeset
     5
This is the ROOT file for a network transmission protocol (NTP
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";