--- 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)"