Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOLCF/IOA/ABP/Impl.thy
author paulson
Wed, 28 Jul 1999 13:52:59 +0200
changeset 7121 0e3d09451b7a
parent 3072 a31419014be5
child 12218 6597093b77e7
permissions -rw-r--r--
removed the unused SeqVar option

(*  Title:      HOLCF/IOA/ABP/Impl.thy
    ID:         $Id$
    Author:     Olaf Mueller
    Copyright   1995  TU Muenchen

The implementation
*)

Impl = Sender + Receiver +  Abschannel +

types 

'm impl_state 
= "'m sender_state * 'm receiver_state * 'm packet list * bool list"
(*  sender_state   *  receiver_state   *    srch_state  * rsch_state *)


constdefs

 impl_ioa    :: ('m action, 'm impl_state)ioa
 "impl_ioa == (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)"

 sen         :: 'm impl_state => 'm sender_state
 "sen == fst"

 rec         :: 'm impl_state => 'm receiver_state
 "rec == fst o snd"

 srch        :: 'm impl_state => 'm packet list
 "srch == fst o snd o snd"

 rsch        :: 'm impl_state => bool list
 "rsch == snd o snd o snd"

end
isabelle