diff -r 37a6e2f55230 -r 44ff2275d44f IOA/example/Sender.thy
--- 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"