IOA/example/Impl.thy
changeset 168 44ff2275d44f
parent 156 fd1be45b64bf
child 249 492493334e0f
--- a/IOA/example/Impl.thy	Wed Nov 09 19:50:36 1994 +0100
+++ b/IOA/example/Impl.thy	Wed Nov 09 19:51:09 1994 +0100
@@ -1,3 +1,11 @@
+(*  Title:      HOL/IOA/example/Impl.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow & Konrad Slind
+    Copyright   1994  TU Muenchen
+
+The implementation
+*)
+
 Impl = Sender + Receiver + Channels +
 
 types 
@@ -17,7 +25,7 @@
  inv3, inv4  :: "'m impl_state => bool"
  hdr_sum     :: "'m packet multiset => bool => nat"
 
-rules
+defs
 
  impl_def
   "impl_ioa == (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)"