src/HOLCF/IOA/ABP/Packet.thy

improved unit theory: unit_all_eq1, unit_all_eq2, split_all_tac;
tuned;

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

Packets
*)

Packet = Arith +

types

   'msg packet = "bool * 'msg"

constdefs

  hdr  :: 'msg packet => bool
  "hdr == fst"

  msg :: 'msg packet => 'msg
  "msg == snd"

end