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