src/HOL/UNITY/Network.thy

--- a/src/HOL/UNITY/Network.thy	Thu Jul 02 16:44:39 1998 +0200
+++ b/src/HOL/UNITY/Network.thy	Thu Jul 02 16:53:55 1998 +0200
@@ -1,5 +1,17 @@
+(*  Title:      HOL/UNITY/Network
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+The Communication Network
+
+From Misra, "A Logic for Concurrent Programming" (1994), section 5.7
+*)
+
 Network = UNITY +
 
+(*The state assigns a number to each process variable*)
+
 datatype pvar = Sent | Rcvd | Idle
 
 datatype pname = Aproc | Bproc