--- a/IOA/example/Sender.thy Wed Nov 09 19:50:36 1994 +0100
+++ b/IOA/example/Sender.thy Wed Nov 09 19:51:09 1994 +0100
@@ -1,4 +1,12 @@
-Sender = IOA + Action + Multiset + List + "Lemmas" +
+(* Title: HOL/IOA/example/Sender.thy
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+
+The implementation: sender
+*)
+
+Sender = IOA + Action + Multiset + List +
types
@@ -15,7 +23,7 @@
sbit :: "'m sender_state => bool"
ssending :: "'m sender_state => bool"
-rules
+defs
sq_def "sq == fst"
ssent_def "ssent == fst o snd"