diff -r 5d9bbc0d9bd3 -r c43ed29bd197 src/HOL/TLA/Buffer/Buffer.thy
--- a/src/HOL/TLA/Buffer/Buffer.thy	Wed Sep 07 20:22:15 2005 +0200
+++ b/src/HOL/TLA/Buffer/Buffer.thy	Wed Sep 07 20:22:39 2005 +0200
@@ -1,15 +1,18 @@
 (*
     File:        Buffer.thy
+    ID:          $Id$
     Author:      Stephan Merz
     Copyright:   1997 University of Munich
 
    Theory Name: Buffer
    Logic Image: TLA
-
-   A simple FIFO buffer (synchronous communication, interleaving)
 *)
 
-Buffer = TLA +
+header {* A simple FIFO buffer (synchronous communication, interleaving) *}
+
+theory Buffer
+imports TLA
+begin
 
 consts
   (* actions *)
@@ -22,21 +25,21 @@
   IBuffer   :: "'a stfun => 'a list stfun => 'a stfun => temporal"
   Buffer    :: "'a stfun => 'a stfun => temporal"
 
-rules
-  BInit_def   "BInit ic q oc    == PRED q = #[]"
-  Enq_def     "Enq ic q oc      == ACT (ic$ ~= $ic) 
-                                     & (q$ = $q @ [ ic$ ]) 
+defs
+  BInit_def:   "BInit ic q oc    == PRED q = #[]"
+  Enq_def:     "Enq ic q oc      == ACT (ic$ ~= $ic)
+                                     & (q$ = $q @ [ ic$ ])
                                      & (oc$ = $oc)"
-  Deq_def     "Deq ic q oc      == ACT ($q ~= #[])
+  Deq_def:     "Deq ic q oc      == ACT ($q ~= #[])
                                      & (oc$ = hd< $q >)
                                      & (q$ = tl< $q >)
                                      & (ic$ = $ic)"
-  Next_def    "Next ic q oc     == ACT (Enq ic q oc | Deq ic q oc)"
-  IBuffer_def "IBuffer ic q oc  == TEMP Init (BInit ic q oc)
+  Next_def:    "Next ic q oc     == ACT (Enq ic q oc | Deq ic q oc)"
+  IBuffer_def: "IBuffer ic q oc  == TEMP Init (BInit ic q oc)
                                       & [][Next ic q oc]_(ic,q,oc)
                                       & WF(Deq ic q oc)_(ic,q,oc)"
-  Buffer_def  "Buffer ic oc     == TEMP (EEX q. IBuffer ic q oc)"
-end
+  Buffer_def:  "Buffer ic oc     == TEMP (EEX q. IBuffer ic q oc)"
 
+ML {* use_legacy_bindings (the_context ()) *}
 
-
+end